val lemma_i2b_eq (#n:pos) (a b:uint_t n) : Lemma
  (requires b_i2b a == b_i2b b)
  (ensures a == b)
let lemma_i2b_eq #n a b =
  assert_norm (b_i2b a == b_i2b b ==> int2bv a == int2bv b);
  int2bv_lemma_2 #n a b
val lemma_i2b_eq (#n:pos) (a b:uint_t n) : Lemma
  (requires b_i2b a == b_i2b b)
  (ensures a == b)
let lemma_i2b_eq #n a b =
assert_norm (b_i2b a == b_i2b b ==> int2bv a == int2bv b);
int2bv_lemma_2 #n a b
Vale.Math.Bits.fst.checked
Vale.Lib.Bv_s.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Vale.Math.Bits.fst
Prims.pos FStar.UInt.uint_t FStar.BV.int2bv_lemma_2 Prims.unit FStar.Pervasives.assert_norm Prims.l_imp Prims.eq2 FStar.BV.bv_t Vale.Math.Bits.b_i2b FStar.BV.int2bv
module Vale.Math.Bits
open FStar.Mul

let lemma_pow2_le m n = FStar.Math.Lemmas.pow2_le_compat n m
val lemma_i2b_eq (#n:pos) (a b:uint_t n) : Lemma
  (requires b_i2b a == b_i2b b)
  (ensures a == b)
a: FStar.UInt.uint_t n -> b: FStar.UInt.uint_t n
  -> FStar.Pervasives.Lemma (requires Vale.Math.Bits.b_i2b a == Vale.Math.Bits.b_i2b b)
      (ensures a == b)