module FStar.UInt

val to_vec_mod_pow2:Unidentified product: [#n:nat] Unidentified product: [a:uint_t n] Unidentified product: [m:pos] Unidentified product: [i:i:nat:{/\(<=(-(n, m), i), <(i, n))}] (Lemma ((requires (==(%(a, pow2 m), 0)))) ((ensures (==(index (to_vec a) i, false)))) (Prims.Cons (SMTPat (index (to_vec #n a) i)) (Prims.Cons (SMTPat (==(%(a, pow2 m), 0))) (Prims.Nil ))))

val to_vec_lt_pow2:Unidentified product: [#n:nat] Unidentified product: [a:uint_t n] Unidentified product: [m:nat] Unidentified product: [i:i:nat:{<(i, -(n, m))}] (Lemma ((requires (<(a, pow2 m)))) ((ensures (==(index (to_vec a) i, false)))) (Prims.Cons (SMTPat (index (to_vec #n a) i)) (Prims.Cons (SMTPat (<(a, pow2 m))) (Prims.Nil ))))

pragma