⊢ ∀t. F ∧ t ⇔ F
⊢ ∀t. t ∧ F ⇔ F
⊢ ∀t. F ∨ t ⇔ t
⊢ ∀t. t ∨ F ⇔ t
⊢ ∀e l. MEM e (e::l)
⊢ ∀l1 e1 e2. MEM e1 l1 ⇒ MEM e1 (e2::l1)
⊢ ∀B A. ¬(A ∧ B) ⇔ ¬A ∨ ¬B
⊢ ∀t. ¬¬t ⇔ t
⊢ ∀B A. ¬(A ∨ B) ⇔ ¬A ∧ ¬B
⊢ ∀t. T ∧ t ⇔ t
⊢ ∀t. t ∧ T ⇔ t
⊢ ∀t. T ∨ t ⇔ T
⊢ ∀t. t ∨ T ⇔ T
⊢ ∀P h t. (∃x. MEM x (h::t) ∧ P x) ⇔ P h ∨ ∃x. MEM x t ∧ P x
⊢ ∀P. (∃x. MEM x [] ∧ P x) ⇔ F
⊢ ∀P y. (∃x. MEM x [y] ∧ P x) ⇔ P y
⊢ ∀p q r. (p ⇒ (q ⇔ r)) ⇒ (p ∧ q ⇔ p ∧ r)
⊢ ∀p q r. (¬p ⇒ (q ⇔ r)) ⇒ (p ∨ q ⇔ p ∨ r)