proposition: Lemma EU_strengthen (p1 q1 p2 q2 : X -> Prop) w : (forall v, p1 v -> p2 v) -> (forall v, q1 v -> q2 v) -> cEU p1 q1 w -> cEU p2 q2 w.
proof: Proof. move => H1 H2. elim => {w} - w; first by move => ?; apply EU0; auto. move => v /H1 wv ? IH. apply: EUs ; auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)