proposition: Lemma proj_keys_Zlength: forall h, Zlength (proj_keys h) = heap_size h.
proof: Proof. intros. unfold proj_keys, heap_size. now rewrite Zlength_map. 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