proposition: Lemma hitem_hitem_: forall v hi, hitem hi v |-- hitem_ v.
proof: Proof. intros. unfold hitem, hitem_. cancel. 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