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