proposition: Lemma uforest'_edgeless_GG: uforest' edgeless_GG.
proof: Proof. split; intros. apply edgeless_GG_evalid in H; contradiction. split; intros. destruct H. destruct H. destruct H. apply edgeless_GG_evalid in H; contradiction. split; intros. apply edgeless_GG_evalid in H; contradiction. unfold unique_simple_upath; intros. destruct H0 as [? [? ?]]. destruct p1. inversion H3. destruct p1. inversion H3. inversion H4. subst u; subst v. destruct H2 as [? [? ?]]. destruct p2. inversion H5. destruct p2. inversion H5. subst v. auto. destruct H2. destruct H2. destruct H2. destruct H2. simpl in H2. contradiction. destruct H0. destruct H0. destruct H0. destruct H0. simpl in H0. contradiction. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.undirected_graph