proposition: Lemma listToGraph'_In: forall g v l e, In e (listEdges (v, l)) -> In (src (listToGraph' g v l) e) (listVertices (v, l)) /\ In (dst (listToGraph' g v l) e) (listVertices (v, l)).
proof: Proof. intros. revert g v e H. induction l; intros; simpl in *. 1: intuition. destruct a. simpl in H. destruct H. 2: apply (IHl (pregraph_add_whole_edge g e0 v v0) v0) in H; simpl; intuition. subst. remember (src (listToGraph' (pregraph_add_whole_edge g e v v0) v0 l) e) as x1. remember (dst (listToGraph' (pregraph_add_whole_edge g e v v0) v0 l) e) as x2. symmetry in Heqx1, Heqx2. pose proof Heqx1. pose proof Heqx2. apply listToGraph'_src in Heqx1. apply listToGraph'_dst in Heqx2. destruct Heqx1. + rewrite addEdge_src_iff in H1. destruct H1 as [[? ?] | [? ?]]. 1: exfalso; tauto. subst v. destruct Heqx2. * rewrite addEdge_dst_iff in H2. destruct H2 as [[? ?] | [? ?]]. 1: exfalso; tauto. subst v0. intuition. * destruct H2. apply (IHl (pregraph_add_whole_edge g e x1 v0)) in H2. destruct H2. rewrite H0 in H4. simpl. intuition. + destruct H1. apply (IHl (pregraph_add_whole_edge g e v v0)) in H1. rewrite H, H0 in H1. simpl. intuition. 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