proposition: Lemma listToGraph'_FiniteGraph: forall g v l, vvalid g v -> FiniteGraph g -> FiniteGraph (listToGraph' g v l).
proof: Proof. intros. destruct X as [[vl [_ ?]] [el [_ ?]]]. unfold Ensembles.In in *. apply Build_FiniteGraph; [exists (nodup equiv_dec (listVertices (v, l) ++ vl)) | exists (nodup equiv_dec (listEdges (v, l) ++ el))]; split; intros. + apply NoDup_nodup. + rewrite nodup_In. unfold Ensembles.In . rewrite in_app_iff, H0, <- list_vertices_vvalid_iff; tauto. + apply NoDup_nodup. + rewrite nodup_In. unfold Ensembles.In . rewrite in_app_iff, H1, <- list_edges_evalid_iff; tauto. 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