⊢ ∀f x. f x = I f x
⊢ ((λx. s x) = t ⇔ ∀x. s x = t x) ∧ (s = (λx. t x) ⇔ ∀x. s x = t x)
⊢ ¬(∃!x. P x) ⇔ (∀x. ¬P x) ∨ ∃x x'. P x ∧ P x' ∧ x ≠ x'
⊢ a ∨ b ∧ c ⇔ (a ∨ b) ∧ (a ∨ c)
⊢ a ∧ b ∨ c ⇔ (a ∨ c) ∧ (b ∨ c)
⊢ (p ⇔ q) ⇔ (p ∨ ¬q) ∧ (¬p ∨ q)
⊢ (p ⇔ q) ⇔ p ∧ q ∨ ¬p ∧ ¬q
⊢ p ⇒ q ⇔ ¬p ∨ q
⊢ ¬(p ∧ q) ⇔ ¬p ∨ ¬q
⊢ (p ⇎ q) ⇔ (p ∨ q) ∧ (¬p ∨ ¬q)
⊢ (p ⇎ q) ⇔ p ∧ ¬q ∨ ¬p ∧ q
⊢ ¬(p ⇒ q) ⇔ p ∧ ¬q
⊢ ¬¬p ⇔ p
⊢ ¬(p ∨ q) ⇔ ¬p ∧ ¬q
⊢ p ⇔ ¬p ⇒ F