proposition: Lemma cAU_cER (p q : X -> Prop) (w : X) : cER (PredC p) (PredC q) w -> ~ cAU p q w.
proof: Proof. move => E A. elim: A E => {w}[w qw|w]; first by case. move => pw _ IH. case => // v _. exact: IH. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)