proposition: Lemma fold_harray': forall L i arr, i = Zlength L -> data_at Tsh (tarray t_item i) (map heap_item_rep L) arr = harray L arr.
proof: Proof. intros. rewrite H. reflexivity. Qed.
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel RelationClasses