proposition: Lemma listToGraph'_dst: forall g v l e x, dst (listToGraph' g v l) e = x -> dst g e = x \/ (In e (listEdges (v, l)) /\ In x (listVertices (v, l))).
proof: Proof. intros. revert g v e x H. induction l; intros; simpl in *. 1: left; auto. destruct a. apply IHl in H. clear IHl. simpl. unfold listEdges, snd in H. destruct H. + rewrite addEdge_dst_iff in H. intuition. + right. destruct H. split; 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