proposition: Lemma wedge_to_cdata_NoDup: forall size (g: @EdgeListGG size), NoDup (map wedge_to_cdata (graph_to_wedgelist g)).
proof: Proof. intros. pose proof (NoDup_g2wedgelist g). apply list_inj_map_NoDup. 2: auto. apply sound_wedge_to_cdata_inj. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist