proposition: Lemma good_path_acyclic: forall (g: Gph) P p n1 n2, path_ends g p n1 n2 -> good_path g P p -> exists p', path_ends g p' n1 n2 /\ NoDup (epath_to_vpath g p') /\ good_path g P p'.
proof: Proof. intros. destruct H0. pose proof H0. apply valid_path_acyclic with (n1 := n1) (n2 := n2) in H0; trivial. destruct H0 as [p' [? [? [? ?]]]]. exists p'. do 3 (split; trivial). apply path_prop_subpath with p; trivial. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec