proposition: Lemma harray_emp: forall arr, heap_array [] arr |-- emp.
proof: Proof. unfold heap_array. intros. rewrite data_at_isptr. entailer. rewrite data_at_zero_array_eq; auto. 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