proposition: Lemma ufroot_same_connected: forall (g: UFGraph) u v, ufroot_same g u v -> connected g u v.
proof: Proof. intros. destruct H as [r [[? _] [? _]]]. apply reachable_implies_connected in H. apply reachable_implies_connected in H0. apply connected_symm in H0. apply (connected_trans _ _ _ _ H H0). Qed.
imports: CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.UnionFind CertiGraph.msl_application.ArrayGraph CertiGraph.unionfind.env_unionfind_arr CertiGraph.graph.undirected_graph