proposition: Lemma rEXn p s t : prv (s ---> t) -> prv (EX p s ---> EX p t).
proof: Proof. move => H. rule ax_contraNN. apply: rNorm. by rule ax_contraNN. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)