proposition: Lemma fold_harray': forall sh L i arr, i = Zlength L -> data_at sh (tarray t_struct_edge i) (map heap_item_rep L) arr = harray sh L arr.
proof: Proof. intros. rewrite H. reflexivity. Qed.
imports: VST.floyd.proofauto Coq.ZArith.ZArith CertiGraph.floyd_ext.closed_lemmas CertiGraph.kruskal.kruskal_edgelist RelationClasses CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel