|- ∀P1 P2 a. (λa. P1 a) a ∧ (λa. P2 a) a ⇔ (λa. P1 a ∧ P2 a) a
|- ∀f P. (∀x y z. P x y ∧ P x z ⇒ P x (f y z)) ∧ (∀x y z. f x (f y z) = f (f x y) z) ∧ (∀x y. P x y ⇒ (f x y = f y x)) ⇒ ∀x y z. P x y ∧ P x z ⇒ (f x (f y z) = f y (f x z))