val lemma_zero_nth (n:nat) : Lemma
  (forall (i:nat{i < n}).{:pattern (nth #n 0 i)} not (nth #n 0 i))
let lemma_zero_nth n =
  let f (i:nat{i < n}) : Lemma (not (nth #n 0 i)) = UInt.zero_nth_lemma #n i in
  FStar.Classical.forall_intro f
val lemma_zero_nth (n:nat) : Lemma
  (forall (i:nat{i < n}).{:pattern (nth #n 0 i)} not (nth #n 0 i))
let lemma_zero_nth n =
let f (i: nat{i < n}) : Lemma (not (nth #n 0 i)) = UInt.zero_nth_lemma #n i in
FStar.Classical.forall_intro f
Vale.Arch.TypesNative.fst.checked
prims.fst.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Vale.Arch.TypesNative.fst
Prims.nat FStar.Classical.forall_intro Prims.b2t Prims.op_LessThan Prims.op_Negation Vale.Arch.TypesNative.nth Prims.unit Prims.l_True Prims.squash FStar.Seq.Base.index Prims.bool FStar.UInt.to_vec Prims.Nil FStar.Pervasives.pattern FStar.UInt.zero_nth_lemma
module Vale.Arch.TypesNative
open FStar.Mul

let lemma_equal_nth n x y =
  UInt.to_vec_lemma_2 #n x y
val lemma_zero_nth (n:nat) : Lemma
  (forall (i:nat{i < n}).{:pattern (nth #n 0 i)} not (nth #n 0 i))
n: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      forall (i: Prims.nat{i < n}). {:pattern Vale.Arch.TypesNative.nth 0 i}
        Prims.op_Negation (Vale.Arch.TypesNative.nth 0 i))