and_def
⊢ $/\ = (λp q. (λf. f p q) = (λf. f T T))
exists_def
⊢ $? = (λP. ∀q. (∀x. P x ⇒ q) ⇒ q)
imp_def
⊢ $==> = (λp q. p ∧ q ⇔ p)