let machine_state_eq (s1 s2:machine_state) =
  s1 == s2
let machine_state_eq (s1 s2: machine_state) =
s1 == s2
Vale.X64.StateLemmas.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_Sems.fsti.checked Vale.X64.Regs.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Flags.fsti.checked Vale.Def.Prop_s.fst.checked Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.Heap.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.FunctionalExtensionality.fsti.checked
Vale.X64.StateLemmas.fsti
Vale.X64.StateLemmas.machine_state Prims.eq2 Prims.logical
module Vale.X64.StateLemmas
open Vale.X64.Machine_s
open Vale.Arch.Heap
open Vale.X64.State
open FStar.FunctionalExtensionality
module Ms = Vale.X64.Machine_Semantics_s
//open Vale.X64.Machine_Semantics_s
//module ME = Vale.X64.Memory
open Vale.X64.Memory
open Vale.Arch.MachineHeap_s
//module MS = Vale.X64.Memory_Sems
module VSS = Vale.X64.Stack_Sems
module F = FStar.FunctionalExtensionality
open Vale.Def.Prop_s
open FStar.Mul

unfold let machine_state = Ms.machine_state
unfold let code = Ms.code
unfold let machine_eval_code = Ms.machine_eval_code
val same_heap_types : squash (vale_full_heap == heap_impl)
unfold let coerce (#b #a:Type) (x:a{a == b}) : b = x
val machine_state_eq : s1: Vale.X64.StateLemmas.machine_state -> s2: Vale.X64.StateLemmas.machine_state -> Prims.logical
s1: Vale.X64.StateLemmas.machine_state -> s2: Vale.X64.StateLemmas.machine_state -> Prims.logical