val lemma_nat_to_two32 (_:unit) : Lemma
  (forall (x:nat64).{:pattern (nat_to_two 32 x)}
    nat_to_two 32 x == Mktwo (x % 0x100000000) (x / 0x100000000))
let lemma_nat_to_two32 () =
  assert_norm (forall (x:nat64).{:pattern (nat_to_two 32 x)}
    nat_to_two 32 x == Mktwo (x % 0x100000000) (x / 0x100000000))
val lemma_nat_to_two32 (_:unit) : Lemma
  (forall (x:nat64).{:pattern (nat_to_two 32 x)}
    nat_to_two 32 x == Mktwo (x % 0x100000000) (x / 0x100000000))
let lemma_nat_to_two32 () =
assert_norm (forall (x: nat64). {:pattern (nat_to_two 32 x)}
      nat_to_two 32 x == Mktwo (x % 0x100000000) (x / 0x100000000))
Vale.Arch.Types.fst.checked
Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.TypesNative.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.Arch.Types.fst
Prims.unit FStar.Pervasives.assert_norm Prims.l_Forall Vale.Def.Words_s.nat64 Prims.eq2 Vale.Def.Words_s.two Vale.Def.Words_s.natN Prims.pow2 Vale.Def.Words.Two_s.nat_to_two Vale.Def.Words_s.Mktwo Prims.op_Modulus Prims.op_Division
module Vale.Arch.Types

open FStar.Mul
open Vale.Def.Opaque_s
open Vale.Def.Types_s
open Vale.Arch.TypesNative
open Vale.Lib.Seqs
open Vale.Def.Words_s
open Vale.Def.Words.Two
open FStar.Calc
val lemma_nat_to_two32 (_:unit) : Lemma
  (forall (x:nat64).{:pattern (nat_to_two 32 x)}
    nat_to_two 32 x == Mktwo (x % 0x100000000) (x / 0x100000000))
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      forall (x: Vale.Def.Words_s.nat64). {:pattern Vale.Def.Words.Two_s.nat_to_two 32 x}
        Vale.Def.Words.Two_s.nat_to_two 32 x ==
        Vale.Def.Words_s.Mktwo (x % 0x100000000) (x / 0x100000000))