module Vale.Arch.HeapLemmas
open FStar.Mul
friend Vale.Arch.Heap

let lemma_heap_impl = ()

let empty_vale_heap_layout_inner h = empty_vale_heap_layout_inner h
let empty_vale_heaplets h = empty_vale_heaplets h

let lemma_heap_ignore_ghost_machine h1 h2 = ()