proposition: Lemma uf_union_ufroot_same: 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, vvalid g1 u -> vvalid g1 v -> uf_union g1 u v g2 -> ufroot_same g2 u v.
proof: Proof. intros. pose proof (uf_union_create_precons _ _ _ _ _ _ H H0). destruct H2 as [u_rt [v_rt [? [? [? [? [? ?]]]]]]]. destruct (EV u_rt v_rt). - rewrite <- e in *. assert (ufroot_same g1 u v). { exists u_rt; split; trivial. } apply (uf_union_affected_inhabited _ _ _ _ _ _ H4 H5) in H1; trivial. destruct H1 as [rt [? ?]]. exists rt. split; apply H9, Union_introl; trivial. - apply (uf_union_affected_inhabited _ _ _ _ _ _ H4 H5) in H1; trivial. destruct H1 as [rt [? ?]]. exists rt. split; apply H8; [apply Union_introl | apply Union_intror]; 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