fact: Definition D1 cls := forall C, C \in cls -> forall p s, [p]s^- \in C -> [some D in cls, reach_demo cls p C D && (s^- \in D)].
imports: Relations Classical_Pred_Type mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.PDL(PDL_def)