proposition: Lemma ufroot_uf_set_in: forall u u_rt, uf_root g u u_rt -> uf_set_in g (ufroot_same u).
proof: Proof. intros. right. exists u_rt. split. - exists u_rt. split; trivial. destruct H; split; trivial. apply reachable_refl. apply (reachable_foot_valid _ _ _ H). - intros. split; intros. + destruct H0 as [? [? ?]]. replace u_rt with x0; trivial. apply (uf_root_unique u); trivial. + exists u_rt; split; 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