proposition: Lemma adjacent_ufroot_same: forall (g: UFGraph) u v, adjacent g u v -> ufroot_same g u v.
proof: Proof. intros. apply adjacent_reachable in H. destruct H. - apply (reachable_ufroot_same _ (liGraph g)); trivial. - apply ufroot_same_symm, (reachable_ufroot_same _ (liGraph g)); trivial. 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