proposition: Lemma uf_equiv_connected: forall (g1 g2: UFGraph) u v, uf_equiv g1 g2 -> connected g1 u v <-> connected g2 u v.
proof: Proof. intros. split; intros. - apply (uf_equiv_connected' g1); trivial. - apply uf_equiv_sym in H. apply (uf_equiv_connected' g2); 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