proposition: Lemma fold_heap_array: forall L arr, data_at Tsh (tarray t_item (Zlength L)) (map heap_item_rep L) arr = heap_array L arr.
proof: Proof. reflexivity. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel