proposition: Lemma pAU_pER (p q : X -> Prop) (w : X) : pER (PredC p) (PredC q) w -> ~ pAU p q w.
proof: Proof. case => pi [pi1 pi2 pi3]. move/(_ pi pi1 pi2). case => n n1 n2. case/(_ n): pi3; last by apply. case => m m1 m2. apply: m2. exact: n1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)