proposition: Corollary connected_by_upath_exists_simple_upath: forall g p u v, connected_by_path g p u v-> exists p', connected_by_path g p' u v /\ simple_upath g p'.
proof: Proof. intros. pose proof (connected_exists_list_edges g p u v H). destruct H0 as [l ?]. pose proof (upath_simplifiable_edges g p l u v H H0). destruct H1 as [p' [? [? [? ?]]]]. exists p'. split; auto. Qed.
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