proposition: Lemma subU t X C A : (sf_closed' F t -> X `<=` F) -> (t |` C,A) \in U -> (X `|` C,A) \in U.
proof: Proof. move => H. rewrite !in_fsetX ![_ && (A \in _)]andbC. case (A \in As) => //=. rewrite !powersetE ![_ `|` C]fsetUC !fsubUset fsub1. case (C `<=` F) => //=. by move/sfc_F. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)