val empty_vale_heap_layout_inner (h:vale_heap) : vale_heap_layout_inner
let empty_vale_heap_layout_inner h = empty_vale_heap_layout_inner h
val empty_vale_heap_layout_inner (h:vale_heap) : vale_heap_layout_inner
let empty_vale_heap_layout_inner h =
empty_vale_heap_layout_inner h
Vale.Arch.HeapLemmas.fst.checked
Vale.Arch.Heap.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Arch.HeapLemmas.fst
Vale.Arch.HeapImpl.vale_heap Vale.Arch.HeapImpl.empty_vale_heap_layout_inner Vale.Arch.HeapImpl.vale_heap_layout_inner
module Vale.Arch.HeapLemmas
open FStar.Mul
friend Vale.Arch.Heap

let lemma_heap_impl = ()
val empty_vale_heap_layout_inner (h:vale_heap) : vale_heap_layout_inner
h: Vale.Arch.HeapImpl.vale_heap -> Vale.Arch.HeapImpl.vale_heap_layout_inner