Theory canonContext

⊢ ∀P. (∃!x. P x) ⇔ ∃x. P x ∧ ∀y. P y ⇒ y = x

⊢ ∀P. P (if a then b else c) ⇔ (¬a ∨ P b) ∧ (a ∨ P c)

⊢ ∀P. P (if a then b else c) ⇔ a ∧ P b ∨ ¬a ∧ P c

⊢ ∀f x. f x = I f x

⊢ a ∨ b ∧ c ⇔ (a ∨ b) ∧ (a ∨ c)

⊢ a ∧ b ∨ c ⇔ (a ∨ c) ∧ (b ∨ c)

⊢ ¬(a ∨ b) ⇒ ¬a

⊢ (¬a ⇔ ¬b) ⇒ (a ⇔ b)

⊢ ¬a ⇒ ¬b ⇒ ¬(a ∨ b)

⊢ ¬(a ∨ b) ⇒ ¬b

⊢ a ∧ (b ∨ c) ⇔ a ∧ b ∨ a ∧ c

⊢ (a ∨ b) ∧ c ⇔ a ∧ c ∨ b ∧ c

⊢ f = (λx. t x) ⇔ ∀x. f x = t x

⊢ (∃x. P) ⇔ P

⊢ z = $@ P ⇒ ($? P ⇔ P z)

⊢ ¬(p ∧ q) ⇔ ¬p ∨ ¬q

⊢ ¬(if p then q else q') ⇔ (p ∨ ¬q') ∧ (¬p ∨ ¬q)

⊢ ¬(if p then q else q') ⇔ p ∧ ¬q ∨ ¬p ∧ ¬q'

⊢ (p ⇎ q) ⇔ (p ∨ q) ∧ (¬p ∨ ¬q)

⊢ (p ⇎ q) ⇔ p ∧ ¬q ∨ ¬p ∧ q

⊢ ¬(p ⇒ q) ⇔ ¬q ∧ p

⊢ ¬¬p ⇔ p

⊢ ¬(p ∨ q) ⇔ ¬p ∧ ¬q

⊢ (if p then q else q') ⇔ (p ∨ q') ∧ (¬p ∨ q)

⊢ (if p then q else q') ⇔ p ∧ q ∨ ¬p ∧ q'

⊢ (p ⇔ q) ⇔ (p ∨ ¬q) ∧ (¬p ∨ q)

⊢ (p ⇔ q) ⇔ p ∧ q ∨ ¬p ∧ ¬q

⊢ p ⇒ q ⇔ q ∨ ¬p

⊢ (¬p ⇒ F) ⇒ p

⊢ (a ∨ b) ∧ c ⇔ a ∧ c ∨ b ∧ c

⊢ P t ⇔ ∀x. x = t ⇒ P x