λ x y z w, q (q (q w))
A → A → A → (∀ w, q (q (q w)) = w)
λ x y z w, q (f (q (q x)) (q (q z)) (q w))
∀ x, A → (∀ z w, q (f (q (q x)) (q (q z)) (q w)) = w)
λ x y z w, q (q (q w))
A → A → A → (∀ w, q (q (q w)) = w)
λ x y z w, w
A → A → A → (∀ w, w = w)