proposition: Lemma listToGraph'_NoDup_In_src: forall g v l e, NoDup (listEdges' Vertex Edge l) -> In e (listEdges' Vertex Edge l) -> exists v', In (v', e) (shiftLeft Vertex Edge v l) /\ src (listToGraph' g v l) e = v'.
proof: Proof. intros. revert g v e H H0. induction l; simpl; intros. 1: exfalso; auto. destruct a. simpl in H0. destruct H0. - subst e0. exists v. simpl. split. + left; auto. + apply NoDup_cons_iff in H. destruct H. apply (listToGraph'_not_In_src (pregraph_add_whole_edge g e v v0) v0) in H. rewrite H. rewrite addEdge_src_iff. right; split; auto. - specialize (IHl (pregraph_add_whole_edge g e0 v v0) v0 e). rewrite NoDup_cons_iff in H. destruct H. specialize (IHl H1 H0). destruct IHl as [v1 [? ?]]. exists v1. split; auto. simpl. right; 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.FiniteGraph