ELIM_PEXISTS2
⊢ (∃p. P (FST p) (SND p) p) ⇔ ∃p1 p2. P p1 p2 (p1,p2)
ELIM_PFORALL2
⊢ (∀p. P (FST p) (SND p) p) ⇔ ∀p1 p2. P p1 p2 (p1,p2)
PEXISTS_THM2
⊢ ∀P. (∃x. $? (P x)) ⇔ $? (UNCURRY P)
PFORALL_THM2
⊢ ∀P. (∀x. $! (P x)) ⇔ $! (UNCURRY P)