proposition: Lemma uf_root_refl: forall x, vvalid g x -> ~ vvalid g (dst g (out_edge x)) -> uf_root g x x.
proof: Proof. intros. split; intros. 1: apply reachable_refl; auto. destruct H1 as [[? ?] ?]. destruct H1 as [[? ?] [? _]]. simpl in H1. subst v. destruct l. 1: simpl in H2; auto. simpl in H3. destruct H3. assert (strong_evalid g e) by (destruct l;[|destruct H3]; auto). clear H3. destruct H4 as [? [? ?]]. symmetry in H1. destruct (only_one_edge _ e H) as [? _]. specialize (H6 (conj H1 H3)). subst e. exfalso; auto. 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