proposition: Lemma initializing_inc_list_done: forall capacity, initializing_inc_list capacity capacity = map (fun z => Vint (Int.repr z)) (List_ext.nat_inc_list (Z.to_nat capacity)).
proof: Proof. unfold initializing_inc_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