proposition: Lemma aAU_inU {C s t H} : (C,aAU (s, t, H)) \in U (sfc (fAU s t^+ |` C `|` \bigcup_(C' in H) C')).
proof: Proof. rewrite -AU_shift; last exact: closed_sfc. apply/andP; split. - apply: power_sub (sub_sfc _). by rewrite powersetE. - rewrite powersetE. apply/subP => D inH. apply: power_sub (sub_sfc _). rewrite powersetE. apply: fsubsetU. by rewrite -[D]/(id D) bigU1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)