proposition: Lemma lst_path_NoDup: forall p x y P, g |= p is x ~o~> y satisfying P -> NoDup (snd p).
proof: Proof. intros. destruct p as [v p]. simpl. destruct (ListDec.NoDup_dec EE p); auto. exfalso. destruct (Dup_cyclic _ n) as [e [p1 [p2 [p3 ?]]]]. subst p. clear n. simpl in H. pose proof H. apply reachable_by_path_app_cons in H0. destruct H0 as [? _]. replace (p1 ++ e :: p2 ++ e :: p3) with ((p1 ++ e :: p2) ++ e :: p3) in H. - apply reachable_by_path_app_cons in H. destruct H as [? _]. apply lst_src_dst_determine_path in H0. destruct H0. apply H1 in H. inversion H. rewrite <- (app_nil_r p1) in H3 at 1. apply app_inv_head in H3. inversion H3. - rewrite <- app_assoc. simpl. auto. Qed.
imports: Coq.Classes.Morphisms Coq.micromega.Lia Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph