proposition: Lemma genU_AUhr s t H C : (C, aAU (s, t, H)) \in U -> (s^+ |` C, aAXU (s, t, C |` H)) \in U.
proof: Proof. rewrite !in_fsetX -AsX !AsAU powersetU -/Cs -andbA. rewrite [_ |` _ \in Hs]powersetU powersetE fsub1 => /and3P [? HF ?]. apply/and5P ; split => //. rewrite powersetE fsub1. move: (sfc_F HF) => /=. by bcase. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)