proposition: Lemma listToGraph'_LF: forall g v l, vvalid g v -> LocalFiniteGraph g -> LocalFiniteGraph (listToGraph' g v l).
proof: Proof. intros. destruct X. apply Build_LocalFiniteGraph. intros. unfold Enumerable, Ensembles.In in *. destruct (local_enumerable x) as [l' [? ?]]. exists (nodup equiv_dec (collectEdges (listToGraph' g v l) x (l' ++ listEdges (v, l)))). split. 1: apply NoDup_nodup. intro e. rewrite nodup_In, collectEdges_In, in_app_iff. rewrite H1. unfold out_edges. rewrite <- list_edges_evalid_iff. intuition. apply listToGraph'_src in H4. 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