proposition: Lemma vgamma_uf_root: forall (g: UFGraph) x r pa root, vvalid g x -> vgamma g x = (r, pa) -> uf_root g x root -> x <> root -> uf_root g pa root.
proof: Proof. intros. pose proof (uf_root_not_eq_root_vgamma g _ _ _ _ H0 H1 H2). destruct H1. split; auto. pose proof (valid_parent g _ _ _ H H0). assert (Decidable (reachable g pa root)) by (apply Graph_reachable_dec; left; auto). apply decidable_prop_decidable in H6. destruct H6; auto. exfalso. pose proof (lst_out_edge_only_one g (liGraph g) x pa root). simpl in H7. apply H2. apply H7; auto. apply (vgamma_not_dst _ _ r); auto. Qed.
imports: Coq.Sets.Ensembles Coq.Lists.List CertiGraph.lib.EquivDec_ext CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph CertiGraph.graph.MathGraph CertiGraph.graph.LstGraph CertiGraph.graph.UnionFind