proposition: Lemma uf_equiv_ufroot_same: forall (g1 g2: UFGraph) u v, uf_equiv g1 g2 -> ufroot_same g1 u v <-> ufroot_same g2 u v.
proof: Proof. intros. do 2 rewrite <- connected_ufroot_same_iff. apply uf_equiv_connected. auto. 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