val bitvec_of_u256_inj (i j:_)
  : Lemma
    (ensures bitvec_of_u256 i == bitvec_of_u256 j ==>
             i == j)
    [SMTPat (bitvec_of_u256 i);
     SMTPat (bitvec_of_u256 j)]
val bitvec_of_u256_inj (i j:_)
  : Lemma
    (ensures bitvec_of_u256 i == bitvec_of_u256 j ==>
             i == j)
    [SMTPat (bitvec_of_u256 i);
     SMTPat (bitvec_of_u256 j)]
let bitvec_of_u256_inj (i j:_)
  : Lemma
    (ensures bitvec_of_u256 i == bitvec_of_u256 j ==>
             i == j)
  = bitvec_of_u64_inj i.v0 j.v0;
    bitvec_of_u64_inj i.v1 j.v1;
    bitvec_of_u64_inj i.v2 j.v2;
    bitvec_of_u64_inj i.v3 j.v3;
    if bitvec_of_u256 i = bitvec_of_u256 j
    then (
    Seq.lemma_append_inj
      (UInt.to_vec (U64.v i.v0))
      ((UInt.to_vec (U64.v i.v1)) `Seq.append` (
       (UInt.to_vec (U64.v i.v2)) `Seq.append` (
       (UInt.to_vec (U64.v i.v3)))))
      (UInt.to_vec (U64.v j.v0))
      ((UInt.to_vec (U64.v j.v1)) `Seq.append` (
       (UInt.to_vec (U64.v j.v2)) `Seq.append` (
       (UInt.to_vec (U64.v j.v3)))));
    Seq.lemma_append_inj
      (UInt.to_vec (U64.v i.v1))
      ((UInt.to_vec (U64.v i.v2)) `Seq.append` (
       (UInt.to_vec (U64.v i.v3))))
      (UInt.to_vec (U64.v j.v1))
       ((UInt.to_vec (U64.v j.v2)) `Seq.append` (
       (UInt.to_vec (U64.v j.v3))));
    Seq.lemma_append_inj
      (UInt.to_vec (U64.v i.v2))
      (UInt.to_vec (U64.v i.v3))
      (UInt.to_vec (U64.v j.v2))
      (UInt.to_vec (U64.v j.v3))
    )
module Zeta.Steel.BitUtils

module T = Zeta.Steel.FormatsManual
module L = FStar.List.Tot
module U64 = FStar.UInt64
module BV = FStar.BV

let bitvec_of_u256 (i:T.u256) : FStar.BitVector.bv_t 256 =
  (UInt.to_vec (U64.v i.v0)) `Seq.append` (
  (UInt.to_vec (U64.v i.v1)) `Seq.append` (
  (UInt.to_vec (U64.v i.v2)) `Seq.append` (
  (UInt.to_vec (U64.v i.v3)))))

let bitvec_of_u64_inj  (i j:U64.t)
  : Lemma
    (ensures
      UInt.to_vec (U64.v i) == UInt.to_vec (U64.v j) ==>
      i == j)
  = UInt.inverse_num_lemma (U64.v i);
    UInt.inverse_num_lemma (U64.v j)
/
Zeta.Steel.FormatsManual.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.BV.fsti.checked FStar.BitVector.fst.checked
Zeta.Steel.BitUtils.fst
i: Zeta.Steel.KeyUtils.u256 -> j: Zeta.Steel.KeyUtils.u256
  -> FStar.Pervasives.Lemma
      (ensures
        Zeta.Steel.BitUtils.bitvec_of_u256 i == Zeta.Steel.BitUtils.bitvec_of_u256 j ==> i == j)
      [SMTPat (Zeta.Steel.BitUtils.bitvec_of_u256 i); SMTPat (Zeta.Steel.BitUtils.bitvec_of_u256 j)]
Zeta.Steel.KeyUtils.u256 Prims.op_Equality Zeta.Steel.BitUtils.bv_t Zeta.Steel.BitUtils.bitvec_of_u256 FStar.Seq.Properties.lemma_append_inj Prims.bool FStar.UInt.to_vec FStar.UInt64.n FStar.UInt64.v Zeta.Steel.KeyUtils.__proj__Mku256__item__v2 Zeta.Steel.KeyUtils.__proj__Mku256__item__v3 Prims.unit Zeta.Steel.KeyUtils.__proj__Mku256__item__v1 FStar.Seq.Base.append Zeta.Steel.KeyUtils.__proj__Mku256__item__v0 Zeta.Steel.BitUtils.bitvec_of_u64_inj Prims.l_True Prims.squash Prims.l_imp Prims.eq2 Prims.Nil FStar.Pervasives.pattern
let bitvec_of_u256_inj (i j: _) : Lemma (ensures bitvec_of_u256 i == bitvec_of_u256 j ==> i == j) =
  
bitvec_of_u64_inj i.v0 j.v0;
bitvec_of_u64_inj i.v1 j.v1;
bitvec_of_u64_inj i.v2 j.v2;
bitvec_of_u64_inj i.v3 j.v3;
if bitvec_of_u256 i = bitvec_of_u256 j
then
  (Seq.lemma_append_inj (UInt.to_vec (U64.v i.v0))
      ((UInt.to_vec (U64.v i.v1))
        `Seq.append`
        ((UInt.to_vec (U64.v i.v2)) `Seq.append` ((UInt.to_vec (U64.v i.v3)))))
      (UInt.to_vec (U64.v j.v0))
      ((UInt.to_vec (U64.v j.v1))
        `Seq.append`
        ((UInt.to_vec (U64.v j.v2)) `Seq.append` ((UInt.to_vec (U64.v j.v3)))));
    Seq.lemma_append_inj (UInt.to_vec (U64.v i.v1))
      ((UInt.to_vec (U64.v i.v2)) `Seq.append` ((UInt.to_vec (U64.v i.v3))))
      (UInt.to_vec (U64.v j.v1))
      ((UInt.to_vec (U64.v j.v2)) `Seq.append` ((UInt.to_vec (U64.v j.v3))));
    Seq.lemma_append_inj (UInt.to_vec (U64.v i.v2))
      (UInt.to_vec (U64.v i.v3))
      (UInt.to_vec (U64.v j.v2))
      (UInt.to_vec (U64.v j.v3)))