fact: Definition graph_list_isomorphism (l: list Vertex) (root: Vertex) : Prop := (forall s d, reachable G root s /\ reachable G root d /\ G |= s ~> d <-> exists l1 l2, l = l1 ++ s :: d :: l2) /\ (forall v, reachable G root v <-> In v l) /\ NoDup l.
imports: Coq.Arith.Arith CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable Coq.Lists.List