val lemma_quad32_vec_equal (a b:quad32) : Lemma
  (requires (
    let Mkfour a0 a1 a2 a3 = a in
    let Mkfour b0 b1 b2 b3 = b in
    equal (UInt.to_vec #32 a0) (UInt.to_vec #32 b0) /\
    equal (UInt.to_vec #32 a1) (UInt.to_vec #32 b1) /\
    equal (UInt.to_vec #32 a2) (UInt.to_vec #32 b2) /\
    equal (UInt.to_vec #32 a3) (UInt.to_vec #32 b3)
  ))
  (ensures a == b)
let lemma_quad32_vec_equal a b =
  let Mkfour a0 a1 a2 a3 = a in
  let Mkfour b0 b1 b2 b3 = b in
  UInt.to_vec_lemma_2 #32 a0 b0;
  UInt.to_vec_lemma_2 #32 a1 b1;
  UInt.to_vec_lemma_2 #32 a2 b2;
  UInt.to_vec_lemma_2 #32 a3 b3;
  ()
val lemma_quad32_vec_equal (a b:quad32) : Lemma
  (requires (
    let Mkfour a0 a1 a2 a3 = a in
    let Mkfour b0 b1 b2 b3 = b in
    equal (UInt.to_vec #32 a0) (UInt.to_vec #32 b0) /\
    equal (UInt.to_vec #32 a1) (UInt.to_vec #32 b1) /\
    equal (UInt.to_vec #32 a2) (UInt.to_vec #32 b2) /\
    equal (UInt.to_vec #32 a3) (UInt.to_vec #32 b3)
  ))
  (ensures a == b)
let lemma_quad32_vec_equal a b =
let Mkfour a0 a1 a2 a3 = a in
let Mkfour b0 b1 b2 b3 = b in
UInt.to_vec_lemma_2 #32 a0 b0;
UInt.to_vec_lemma_2 #32 a1 b1;
UInt.to_vec_lemma_2 #32 a2 b2;
UInt.to_vec_lemma_2 #32 a3 b3;
()
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
Vale.Def.Types_s.quad32 Vale.Def.Types_s.nat32 Prims.unit FStar.UInt.to_vec_lemma_2
module Vale.Arch.TypesNative
open FStar.Mul

let lemma_equal_nth n x y =
  UInt.to_vec_lemma_2 #n x y

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 //(UInt.zero_nth_lemma #n)
val lemma_quad32_vec_equal (a b:quad32) : Lemma
  (requires (
    let Mkfour a0 a1 a2 a3 = a in
    let Mkfour b0 b1 b2 b3 = b in
    equal (UInt.to_vec #32 a0) (UInt.to_vec #32 b0) /\
    equal (UInt.to_vec #32 a1) (UInt.to_vec #32 b1) /\
    equal (UInt.to_vec #32 a2) (UInt.to_vec #32 b2) /\
    equal (UInt.to_vec #32 a3) (UInt.to_vec #32 b3)
  ))
  (ensures a == b)
a: Vale.Def.Types_s.quad32 -> b: Vale.Def.Types_s.quad32
  -> FStar.Pervasives.Lemma
      (requires
        (let _ = a in
          (let { lo0 = a0 ; lo1 = a1 ; hi2 = a2 ; hi3 = a3 } = _ in
            let _ = b in
            (let { lo0 = b0 ; lo1 = b1 ; hi2 = b2 ; hi3 = b3 } = _ in
              FStar.Seq.Base.equal (FStar.UInt.to_vec a0) (FStar.UInt.to_vec b0) /\
              FStar.Seq.Base.equal (FStar.UInt.to_vec a1) (FStar.UInt.to_vec b1) /\
              FStar.Seq.Base.equal (FStar.UInt.to_vec a2) (FStar.UInt.to_vec b2) /\
              FStar.Seq.Base.equal (FStar.UInt.to_vec a3) (FStar.UInt.to_vec b3))
            <:
            Type0)
          <:
          Type0)) (ensures a == b)