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