val bitvec_of_u64_inj (i j: U64.t)
    : Lemma (ensures UInt.to_vec (U64.v i) == UInt.to_vec (U64.v j) ==> i == j)
val bitvec_of_u64_inj (i j: U64.t)
    : Lemma (ensures UInt.to_vec (U64.v i) == UInt.to_vec (U64.v j) ==> i == j)
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)
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)))))
/
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: FStar.UInt64.t -> j: FStar.UInt64.t
  -> FStar.Pervasives.Lemma
    (ensures FStar.UInt.to_vec (FStar.UInt64.v i) == FStar.UInt.to_vec (FStar.UInt64.v j) ==> i == j
    )
FStar.UInt64.t FStar.UInt.inverse_num_lemma FStar.UInt64.n FStar.UInt64.v Prims.unit Prims.l_True Prims.squash Prims.l_imp Prims.eq2 FStar.BitVector.bv_t FStar.UInt.to_vec Prims.Nil FStar.Pervasives.pattern
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)