proposition: Lemma harray_emp: forall arr, harray [] arr |-- emp.
proof: Proof. unfold harray. intros. rewrite data_at_isptr. entailer. rewrite data_at_zero_array_eq; auto. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel RelationClasses