proposition: Lemma uf_union_joins_only_uv: forall (g1 g2: PreGraph Vertex Edge) (li1 : LstGraph g1 out_edge) (li2 : LstGraph g2 out_edge) (fin1: FiniteGraph g1) (fin2: FiniteGraph g2) (ma1: MathGraph g1 is_null) (ma2: MathGraph g2 is_null)u v x y, vvalid g1 u -> vvalid g1 v -> vvalid g1 x -> vvalid g1 y -> uf_union g1 u v g2 -> ~ ufroot_same g1 x u -> ~ ufroot_same g1 x v -> ~ ufroot_same g1 x y -> ~ ufroot_same g2 x y.
proof: Proof. intros. pose proof (uf_union_create_precons _ _ _ _ _ _ H H0). destruct H7 as [u_rt [v_rt [? [? [? [? [? ?]]]]]]]. assert (ufroot_same g1 x x). { apply (ufroot_same_refl _ li1); trivial. } apply (uf_union_unaffected_inhabited _ _ _ _ _ _ _ _ H9 H10 H13) in H3; trivial. destruct H3 as [rt [? ?]]. rewrite H14 in *. intro. apply H6. apply (ufroot_same_uf_root_trans _ li2 x); trivial. - intro. apply (same_set_contra _ _ _ x H14); trivial. intro. apply H4. apply ufroot_same_symm; trivial. - intro. apply (same_set_contra _ _ _ x H14); trivial. intro. apply H5. apply ufroot_same_symm; trivial. - apply (vvalid_get_ufroot _ li1) in H1. destruct H1 as [x_rt ?]. apply (ufroot_uf_set_in _ li1 x x_rt); trivial. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.Ensembles_ext CertiGraph.lib.EnumEnsembles CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.FiniteGraph CertiGraph.graph.reachable_computable