proposition: Lemma genU_aAXR s t H C : (C, aAXR (s, t, H)) \in U -> (R C, aAR (s, t, H)) \in U.
proof: Proof. rewrite !in_fsetX AsX'. case: (aAXR _ \in _) => //; rewrite ?andbF // !andbT. exact: RinU. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)