proposition: Lemma genU_AXn s C E : (fAX s^- |` C , E) \in U -> (s^- |` R C, aR E) \in U.
proof: Proof. rewrite !in_fsetX => /andP [C1 C2]. rewrite genU_aR // andbT. move: C1. rewrite powersetU powersetE fsub1 => /andP [/sfc_F ? /RinU ?]. rewrite powersetU powersetE fsub1. by apply/andP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)