proposition: Lemma cEU_eq (x y : X) (p q : pred X) : p x = p y -> q x = q y -> e x =p e y -> cEU p q x -> cEU p q y.
proof: Proof. move => Hp Hq Ht. case => [?|z xz Hs]; first by apply: EU0; congruence. apply: EUs => //. congruence. exact/Ht. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)