proposition: Lemma EST_root_reachable_by: forall (g1 g2: Graph) (e: E) (root: V) (P: V -> Prop), out_edges g1 root e -> vvalid g1 root -> P root -> ReachDecidable g1 (dst g1 e) (fun x => P x /\ x <> root) -> edge_spanning_tree g1 e (fun x => P x /\ x <> root) g2 -> Included (reachable_by g2 root P) (reachable_by g1 root P).
proof: Proof. intros. destruct H2 as [[? ?] | [? ?]]. + apply (spanning_tree_root_reachable_by g1 g2 e); auto. + intro n. unfold Ensembles.In . intros. rewrite (gremove_root_reachable_by_equiv g1 g2 e); auto. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind Coq.Logic.Classical