MONO_EXISTS
⊢ (∀x. P x ⇒ Q x) ⇒ $? P ⇒ $? Q
MONO_FORALL
⊢ (∀x. P x ⇒ Q x) ⇒ $! P ⇒ $! Q
MONO_RESEXISTS
⊢ (∀x. P x ⇒ P' x) ∧ (∀x. Q x ⇒ Q' x) ⇒ RES_EXISTS P Q ⇒ RES_EXISTS P' Q'
MONO_RESFORALL
⊢ (∀x. P' x ⇒ P x) ∧ (∀x. Q x ⇒ Q' x) ⇒ RES_FORALL P Q ⇒ RES_FORALL P' Q'