proposition: Lemma connected_ufroot_same_iff: forall (g: UFGraph) u v, connected g u v <-> ufroot_same g u v.
proof: Proof. intros. split; intros. apply connected_ufroot_same; trivial. apply ufroot_same_connected; 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