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. rewrite connected_exists_path in H0. destruct H0 as [p [? [? ?]]]. generalize dependent u. induction p. - intros. inversion H1. - destruct p. + intros. simpl in H1, H2. inversion H1. inversion H2. subst. apply connected_refl; trivial. simpl in H0. destruct H. apply H; trivial. + destruct H0. rewrite last_error_cons in H2. 2: unfold not; inversion 1. specialize (IHp H1 H2). intros. simpl in H3. inversion H3; subst a; clear H3. assert (connected g2 z v). { apply adjacent_requires_vvalid in H0. destruct H0. apply IHp; trivial. } apply (uf_equiv_adjacent_connected _ g2) in H0; trivial. apply (connected_trans _ _ _ _ H0 H3). 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