proposition: Lemma uforest'_edgeless_graph: uforest' edgeless_graph.
proof: Proof. split; intros. apply edgeless_graph_evalid in H; contradiction. split; intros. destruct H. destruct H. destruct H. apply edgeless_graph_evalid in H; contradiction. split; intros. apply edgeless_graph_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.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph