proposition: Lemma w2c2w_map: forall l, (forall w, In w l -> Int.min_signed <= fst w <= Int.max_signed /\ Int.min_signed <= fst (snd w) <= Int.max_signed /\ Int.min_signed <= snd (snd w) <= Int.max_signed) -> map cdata_to_wedge (map wedge_to_cdata l) = l.
proof: Proof. intros. induction l. simpl; auto. rewrite map_cons. rewrite map_cons. assert (In a (a::l)) by (left;auto). apply H in H0. destruct H0 as [? [? ?]]. rewrite w2c2w; auto. apply cons_eq. apply IHl. intros. apply H. right; auto. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist