val va_code_Mem64_lemma : va_dummy:unit -> Tot va_code
let va_code_Mem64_lemma () =
  (va_Block (va_CNil ()))
val va_code_Mem64_lemma : va_dummy:unit -> Tot va_code
let va_code_Mem64_lemma () =
(va_Block (va_CNil ()))
Vale.X64.InsMem.fst.checked
Vale.X64.Taint_Semantics.fst.checked Vale.X64.StateLemmas.fsti.checked Vale.X64.Print_s.fst.checked Vale.X64.Memory_Sems.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.InsLemmas.fsti.checked Vale.X64.Decls.fst.checked Vale.Lib.Seqs.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.X64.InsMem.fst
Prims.unit Vale.X64.Decls.va_Block Vale.X64.Decls.va_CNil Vale.X64.Decls.va_code
module Vale.X64.InsMem
open Vale.X64
open Vale.X64.StateLemmas
open Vale.X64.InsLemmas
open Vale.Arch.Heap
open Vale.Arch.HeapImpl
module I = Vale.X64.Instructions_s
module S = Vale.X64.Machine_Semantics_s
module P = Vale.X64.Print_s
open Vale.X64.Taint_Semantics

friend Vale.X64.Decls
#reset-options "--initial_fuel 2 --max_fuel 2 --max_ifuel 2 --z3rlimit 20"
//-- Mem64_in
//--
//-- Mem64_lemma

[@ "opaque_to_smt"]
val va_code_Mem64_lemma : va_dummy:unit -> Tot va_code
va_dummy: Prims.unit -> Vale.X64.Decls.va_code