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