proposition: Lemma aAXR_inU {C s t H} : (C,aAXR (s, t, H)) \in U (sfc (fAR s t^- |` C `|` \bigcup_(C' in H) C')).
proof: Proof. rewrite in_fsetX -AsX' -in_fsetX -/(U _). exact: aAR_inU. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)