proposition: Lemma genU_AUhl s t H C : (C, aAU (s, t, H)) \in U -> (t^+ |` C, aVoid) \in U.
proof: Proof. rewrite -AU_shift => /andP [A _]. apply: (@genU_AUpl s). by rewrite in_fsetX AsV. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)