proposition: Lemma pER_strengthen (p1 q1 p2 q2 : X -> Prop) w : (forall v, p1 v -> p2 v) -> (forall v, q1 v -> q2 v) -> pER p1 q1 w -> pER p2 q2 w.
proof: Proof. move => Hp Hq [pi [? ? Hpi]]. exists pi. split => // n. by case: (Hpi n); firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)