proposition: Lemma uf_union_remains_disjoint2: 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 a, vvalid g1 u -> vvalid g1 v -> vvalid g1 a -> uf_union g1 u v g2 -> ~ ufroot_same g1 a u -> ~ ufroot_same g1 a v -> ~ ufroot_same g2 a v.
proof: Proof. intros. apply uf_union_sym in H2. apply (uf_union_remains_disjoint1 g1) with (v := u); 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