proposition: Lemma forest_edge': forall p l g e, uforest' g -> strong_evalid g e -> connected_by_path g p (src g e) (dst g e) -> fits_upath g l p -> In e l.
proof: Proof. intros. pose proof (upath_simplifiable_edges g p l (src g e) (dst g e) H1 H2). destruct H3 as [p' [l' [? [? [? [? ?]]]]]]. pose proof (trivial_path1 g e H0). destruct H8 as [? ?]. assert (simple_upath g ((src g e)::(dst g e)::nil)). split. apply H8. apply NoDup_cons. unfold not; intros; destruct H10. symmetry in H10. apply H in H10. contradiction. apply H0. simpl in H10; contradiction. apply NoDup_cons. unfold not; intros. simpl in H10; contradiction. apply NoDup_nil. assert (p' = (src g e :: dst g e :: nil)). destruct H as [? [? [? ?]]]. apply (H13 (src g e) (dst g e)); auto. subst p'. apply H7. destruct l'. simpl in H6; contradiction. destruct l'. 2: { simpl in H6. destruct H6. contradiction. } left. destruct H9. destruct H6. destruct H as [? [? ?]]. apply (H13 (src g e) (dst g e)). split; 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