proposition: Lemma listToGraph'_not_In: forall g v l e, ~ In e (listEdges (v, l)) -> src (listToGraph' g v l) e = src g e /\ dst (listToGraph' g v l) e = dst g e.
proof: Proof. intros g v l. revert g v. induction l; intros; simpl in *; auto. destruct a. simpl in H. assert (~ In e (listEdges (v0, l))) by (unfold listEdges, snd; intro; apply H; right; auto). apply (IHl (pregraph_add_whole_edge g e0 v v0)) in H0. destruct H0. rewrite H0, H1. simpl. unfold updateEdgeFunc. destruct (equiv_dec e0 e); auto. hnf in e1. exfalso; apply H. left; 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