proposition: Lemma c2w2c: forall wedgerep, def_wedgerep wedgerep -> wedge_to_cdata (cdata_to_wedge wedgerep) = wedgerep.
proof: Proof. unfold def_wedgerep; intros. destruct H as [? [? ?]]. destruct (fst wedgerep) eqn:Hw; try contradiction. destruct (fst (snd wedgerep)) eqn:Hu; try contradiction. destruct (snd (snd wedgerep)) eqn:Hv; try contradiction. replace wedgerep with (Vint i, (Vint i0, Vint i1)). 2: { rewrite <- Hw; rewrite <- Hu; rewrite <- Hv. destruct wedgerep as [? [? ?]]; auto. } unfold wedge_to_cdata; unfold cdata_to_wedge; simpl. repeat rewrite Int.repr_signed; auto. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist