proposition: Corollary uforest'_no_simple_ucycle: forall g p l, uforest' g -> ~ simple_ucycle g p l.
proof: Proof. unfold uforest, not; intros. destruct H0. destruct p. contradiction. destruct p. contradiction. destruct H1 as [? [? ?]]. destruct l. contradiction. apply (uforest'_no_simple_ucycles g H (v::v0::p) (e::l)). apply H1. auto. split. auto. split. auto. split. auto. auto. Qed.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph