proposition: Lemma uf_root_gen_dst_diff: 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 x_root -> uf_root (pregraph_gen_dst g (out_edge x_root) y_root) z y_root.
proof: Proof. intros. apply uf_root_gen_dst. - destruct H0. split; [apply reachable_refl; apply reachable_foot_valid with y; auto | apply H3]. - intro. apply H1. destruct H0. symmetry. apply H4; auto. - destruct H2; 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