proposition: Lemma genU_AUpr s t C E : (fAU s t^+ |` C,E) \in U -> ([fset s^+, fAX (fAU s t)^+ & C],E) \in U.
proof: Proof. rewrite fsetUA. apply: subU => /=. case/and3P => []; auto with fset. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)