proposition: Lemma uf_union_refl: forall (g: Graph) x y root, uf_root g x root -> uf_root g y root -> uf_union g x y g.
proof: Proof. intros. split; [|split]; intros; auto. unfold uf_set_in in *. destruct H3, H4. - left. rewrite H3. rewrite H4. rewrite Union_Empty_left. reflexivity. - pose proof (app_same_set H3). rewrite H5 in H1. inversion H1. - pose proof (app_same_set H4). rewrite H5 in H2. inversion H2. - destruct H3 as [rt1 [? ?]]. destruct H4 as [rt2 [? ?]]. assert (rt1 = root). { rewrite H5 in H1. apply (@uf_root_unique _ _ _ _ g _ (P_Lst g (sound_gg g)) x); auto. } subst rt1. assert (rt2 = root) by (rewrite H6 in H2; apply (@uf_root_unique _ _ _ _ g _ (P_Lst g (sound_gg g)) y); auto). subst rt2. right. exists root. split. 1: apply Union_introl; unfold In; auto. intro z. rewrite Union_spec. rewrite H5, H6. intuition. 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