proposition: Lemma ER_strengthen (p1 q1 p2 q2 : X -> Prop) w : (forall v, p1 v -> p2 v) -> (forall v, q1 v -> q2 v) -> cER p1 q1 w -> cER p2 q2 w.
proof: Proof. move => Hp Hq. move: w. cofix ER_strengthen => w. case => [/Hp ? /Hq ?|v V1 V2 V3]; first exact: ER0. by apply: ERs _ V2 _ ; auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)