proposition: Lemma uf_equiv_adjacent_connected: forall (g1 g2 : UFGraph) u v, uf_equiv g1 g2 -> adjacent g1 u v -> connected g2 u v.
proof: Proof. intros. apply adjacent_reachable in H0. destruct H0. - apply (reachable_uf_equiv_connected g1); trivial. - apply connected_symm. apply (reachable_uf_equiv_connected g1); 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