fact: Definition adjacent_hd g (u: V) (v: option V) := match v with | None => vvalid g u | Some v' => adjacent g u v' end.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph