proposition: Lemma gToLst_lstToG_eq: forall v l, NoDup (listVertices (v, l)) -> NoDup (listEdges (v, l)) -> graphToList (listToGraph (v, l)) (listToGraph_vva (v, l)) (listToGraphLF (v, l)) (length l) v = (v, l).
proof: Proof. intros. unfold graphToList. f_equal. remember (listToGraph_vva (v, l)) as VVA. clear HeqVVA. remember (listToGraphLF (v, l)) as LF. clear HeqLF. unfold listToGraph in *. rewrite gToLst_lstToG_eq'; auto. + rewrite app_nil_r. apply rev_involutive. + simpl; auto. + simpl; intuition. + intros. unfold out_edges. simpl. intro. destruct H2; 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