let heaplet_id = heaplet_id
let heaplet_id =
heaplet_id
Vale.X64.Memory.fsti.checked
Vale.X64.Machine_s.fst.checked Vale.Lib.Map16.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.BigOps.fsti.checked
Vale.X64.Memory.fsti
Vale.Arch.HeapImpl.heaplet_id
module Vale.X64.Memory
include Vale.Arch.HeapTypes_s
open FStar.Mul
open Vale.Def.Prop_s
open Vale.X64.Machine_s
open Vale.Arch.HeapImpl
module Map16 = Vale.Lib.Map16

unfold let vale_heap = vale_heap
val heaplet_id : Type0
Type0