proposition: Lemma AsX p H : (aAU (p, H) \in As) = (aAXU (p, H) \in As).
proof: Proof. rewrite /As !inE !eqF //= !in_fimset2 ?curryE ?in_fimset2F //; split; congruence. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def gen_def)