proposition: Lemma in_Req u C : fAX u^- \in C -> u^-|` R C \in Req C.
proof: Proof. move => H. rewrite !inE;rightb. apply/fimsetP. by exists (fAX u^-); rewrite ?inE ?H. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)