fact: Definition unique_simple_upath g := (forall u v p1 p2, simple_upath g p1 -> connected_by_path g p1 u v -> simple_upath g p2 -> connected_by_path g p2 u v -> p1 = p2).
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