proposition: Lemma gremove_root_reachable_by_equiv: forall (g1 g2: Graph) (e: E) (root: V) (P: V -> Prop), out_edges g1 root e -> gremove_edge g1 e g2 -> (~ (P (dst g1 e) /\ dst g1 e <> root)) -> forall n, (g1 |= root ~o~> n satisfying P <-> g2 |= root ~o~> n satisfying P).
proof: Proof. intros. split; intros; destruct H. + rewrite reachable_acyclic in H2. destruct H2 as [p [? ?]]. exists p. apply (gremove_reachable_by_derive g1 e); auto. intros. destruct p as [v p]. simpl in H5. intro. subst. apply H1. clear H1. destruct H4 as [[? ?] [? ?]]. split. - rewrite (path_prop_equiv _ _ _ H4) in H6. apply H6. right. exists e. simpl. split; auto. - cut (src g1 e <> dst g1 e). intuition. apply NoDup_epath_to_vpath_edge with (v, p); auto. + destruct H2 as [p ?]. exists p. apply (gremove_not_reachable_by_derive _ e g2); 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