proposition: Lemma uf_root_gen_dst_diff_preserve: forall x y x_root y_root z, uf_root g x x_root -> uf_root g y y_root -> x_root <> y_root -> uf_root g z y_root -> uf_root (pregraph_gen_dst g (out_edge x_root) y_root) z y_root.
proof: Proof. intros. apply uf_root_gen_dst_preserve; auto. - destruct H. apply reachable_foot_valid in H; auto. - intro. apply H1. destruct H2. destruct (lst_reachable_or g _ _ _ _ H3 H2); [destruct H | destruct H0; symmetry]; apply H6; 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