proposition: Lemma def_wedgerep_map_w2c: forall size (g: @EdgeListGG size), Forall def_wedgerep (map wedge_to_cdata (graph_to_wedgelist g)).
proof: Proof. intros. rewrite Forall_forall; intros. apply list_in_map_inv in H. destruct H as [? [? _]]. unfold wedge_to_cdata in H. unfold def_wedgerep. rewrite (surjective_pairing x) in *. inversion H; clear H. destruct x. rewrite (surjective_pairing c) in *. simpl fst in *; simpl snd in *. inversion H2; clear H2. rewrite H1, H0, H3. split3; trivial. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist