proposition: Lemma reachable_by_through_singleton: forall g P n1 n2, reachable_by_through_set g (n1 :: nil) P n2 <-> g |= n1 ~o~> n2 satisfying P.
proof: Proof. intros. unfold reachable_by_through_set; split; intro. + destruct H as [s [? ?]]. simpl in H. destruct H; [subst | exfalso]; auto. + exists n1. split; [apply in_eq | auto]. 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