proposition: Lemma edge_P_reachable_by: forall (g: Gph) n1 n2 (P: Ensemble V), P n1 -> P n2 -> g |= n1 ~> n2 -> g |= n1 ~o~> n2 satisfying P.
proof: Proof. intros. destruct H1 as [? [? ?]]. rewrite step_spec in H3. destruct H3 as [e [? [? ?]]]. exists (n1, e :: nil). split; split; auto. - simpl. split; auto. split; intuition. rewrite H4. auto. rewrite H5; auto. - red. simpl. rewrite Forall_forall. subst. split; intros; auto. simpl in H4. destruct H4. 2: easy. subst. easy. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec