proposition: Lemma graph_gen_redirect_parent_equiv: forall (g1 g2: UFGraph) x r pa root (Hv: vvalid g2 x) (Hn: ~ reachable g2 root x), vvalid g1 x -> vgamma g1 x = (r, pa) -> pa <> x -> uf_equiv g1 g2 -> uf_root g2 pa root -> uf_equiv g1 (pregraph_gen_dst g2 (out_edge x) root).
proof: Proof. intros. apply graph_gen_redirect_parent_equiv'; auto. rewrite <- (uf_equiv_root_the_same g1); auto. apply (uf_root_edge g1 (liGraph g1) x pa); [| apply (vgamma_not_dst g1 x r) | rewrite (uf_equiv_root_the_same g1 g2)]; 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