proposition: Lemma rep2hi_map_ok: forall L, Forall def_wedgerep L -> map (heap_item_rep oo rep2hi) L = L.
proof: Proof. induction L. trivial. simpl. intro. inversion H. rewrite IHL; auto. subst. f_equal. rewrite rep2hi_ok. trivial. rewrite Forall_forall in H. apply H. left. trivial. Qed.
imports: VST.floyd.proofauto CertiGraph.floyd_ext.share CertiGraph.lib.List_ext CertiGraph.unionfind.env_unionfind_arr RelationClasses CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel Sorting CertiGraph.kruskal.spatial_wedgearray_graph CertiGraph.kruskal.kruskal_specs