proposition: Lemma rep2hi_ok: forall r, def_wedgerep r -> heap_item_rep (rep2hi r) = r.
proof: Proof. destruct r as [? [? ?]]. simpl in *. intros [? [? ?]]. simpl in *. destruct y; destruct y0; destruct c; try contradiction. 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