proposition: Lemma c2w2c_map: forall (l: list (reptype t_struct_edge)), Forall def_wedgerep l -> map wedge_to_cdata (map cdata_to_wedge l) = l.
proof: Proof. induction l; intros. simpl; auto. rewrite map_cons. rewrite map_cons. rewrite c2w2c. apply cons_eq. apply IHl. apply Forall_inv_tail in H. auto. apply Forall_inv in H; auto. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist