proposition: Lemma fold_harray: forall sh L arr, data_at sh (tarray t_struct_edge (Zlength L)) (map heap_item_rep L) arr = harray sh L arr.
proof: Proof. 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