val lemma_equal_nth (n:pos) (x y:natN (pow2 n)) : Lemma
  (requires (forall (i:nat).{:pattern (nth #n x i) \/ (nth #n y i)} i < n ==> nth #n x i == nth #n y i))
  (ensures x == y)
let lemma_equal_nth n x y =
  UInt.to_vec_lemma_2 #n x y
val lemma_equal_nth (n:pos) (x y:natN (pow2 n)) : Lemma
  (requires (forall (i:nat).{:pattern (nth #n x i) \/ (nth #n y i)} i < n ==> nth #n x i == nth #n y i))
  (ensures x == y)
let lemma_equal_nth n x y =
UInt.to_vec_lemma_2 #n x y
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.pos Vale.Arch.TypesNative.natN Prims.pow2 FStar.UInt.to_vec_lemma_2 Prims.unit
module Vale.Arch.TypesNative
open FStar.Mul
val lemma_equal_nth (n:pos) (x y:natN (pow2 n)) : Lemma
  (requires (forall (i:nat).{:pattern (nth #n x i) \/ (nth #n y i)} i < n ==> nth #n x i == nth #n y i))
  (ensures x == y)

    n: Prims.pos ->
    x: Vale.Arch.TypesNative.natN (Prims.pow2 n) ->
    y: Vale.Arch.TypesNative.natN (Prims.pow2 n)
  -> FStar.Pervasives.Lemma
      (requires
        forall (i: Prims.nat).
          {:pattern Vale.Arch.TypesNative.nth x i\/Vale.Arch.TypesNative.nth y i}
          i < n ==> Vale.Arch.TypesNative.nth x i == Vale.Arch.TypesNative.nth y i) (ensures x == y)