proposition: Lemma list_vertices_vvalid: forall g v l x, vvalid g v -> In x (listVertices (v, l)) -> vvalid (listToGraph' g v l) x.
proof: Proof. intros. destruct (equiv_dec v x). + hnf in e. subst v. clear H0. apply listToGraph'_preserve_vvalid; auto. + compute in c. revert g v H H0 c. induction l; intros. 1: simpl in *; destruct H0; exfalso; auto. destruct a; simpl in *. destruct H0. 1: exfalso; auto. destruct (equiv_dec v0 x). - hnf in e0. subst. apply listToGraph'_preserve_vvalid, addEdge_add_vvalid. - compute in c0. destruct H0. 1: exfalso; auto. apply IHl; auto. apply addEdge_add_vvalid. 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