proposition: Lemma AXR_shift s t C H : (fAX (fAR s t)^- |` C \in Cs) && (H \in Hs) = ((C,aAXR (s,t,H)) \in U).
proof: Proof. by rewrite in_fsetX AsAXR powersetU powersetE fsub1 -/Cs; bcase. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)