Theorems
⊢ (∀t. T ∧ t ⇔ t) ∧ (∀t. t ∧ T ⇔ t) ∧ (∀t. F ∧ t ⇔ F) ∧ (∀t. t ∧ F ⇔ F) ∧
∀t. t ∧ t ⇔ t
⊢ (∀t. (T ⇔ t) ⇔ t) ∧ (∀t. (t ⇔ T) ⇔ t) ∧ (∀t. (F ⇔ t) ⇔ ¬t) ∧
(∀t. (t ⇔ F) ⇔ ¬t) ∧ ∀t. (t ⇔ t) ⇔ T
⊢ (∀t1 t2. (if T then t1 else t2) = t1) ∧
(∀t1 t2. (if F then t1 else t2) = t2) ∧ ∀b t. (if b then t else t) = t
⊢ (∀t. T ⇒ t ⇔ t) ∧ (∀t. t ⇒ T ⇔ T) ∧ (∀t. F ⇒ t ⇔ T) ∧ (∀t. t ⇒ F ⇔ ¬t) ∧
∀t. t ⇒ t ⇔ T
⊢ (¬T ⇔ F) ∧ (¬F ⇔ T) ∧ ∀t. ¬¬t ⇔ t
⊢ (∀t. T ∨ t ⇔ T) ∧ (∀t. t ∨ T ⇔ T) ∧ (∀t. F ∨ t ⇔ t) ∧ (∀t. t ∨ F ⇔ t) ∧
∀t. t ∨ t ⇔ t