proposition: Lemma Fsub s t X : t \in ssub s -> s \in X -> X \in U -> t \in F.
proof: Proof. Proof using sfc_F. move => Hsub sX XU. rewrite powersetE in XU. have/(sf_ssub sfc_F)/subP : s \in F by exact: (subP XU). by apply. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)