proposition: Lemma NoDup_epath_to_vpath_edge: forall g p, valid_path g p -> NoDup (epath_to_vpath g p) -> forall e, In e (snd p) -> src g e <> dst g e.
proof: Proof. intros g p. destruct p as [v p]. revert v; induction p; intros. 1: simpl in H1; inversion H1. simpl in H1. destruct H1. + subst. simpl in H. destruct H. simpl in H0. destruct p. - apply NoDup_cons_2 in H0. intro. apply H0. rewrite H2. apply in_eq. - destruct H1 as [? [? ?]]. apply NoDup_cons_2 in H0. intro. apply H0. clear H0. rewrite H4. rewrite H2. destruct p; apply in_eq. + rewrite valid_path_cons_iff in H. destruct H as [? [? ?]]. rewrite epath_to_vpath_cons_eq in H0; auto. unfold snd in IHp. apply IHp with (dst g a); auto. apply NoDup_cons_1 in H0. auto. 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