proposition: Lemma initializing_item_list_done: forall capacity, initializing_item_list capacity capacity = map heap_item_rep (initial_item_list capacity).
proof: Proof. unfold initializing_item_list. intros. rewrite Z.sub_diag. apply app_nil_r. 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