∀abstraction:Univ.
∀apply:∀_:Univ.∀_:Univ.Univ.
∀b:∀_:Univ.Univ.
∀c:∀_:Univ.Univ.
∀k:Univ.
∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply abstraction X) Y) Z) (apply (apply X (apply k Z)) (apply Y Z)).
∀abstraction:Univ.
∀apply:∀_:Univ.∀_:Univ.Univ.
∀b:∀_:Univ.Univ.
∀c:∀_:Univ.Univ.
∀k:Univ.
∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply abstraction X) Y) Z) (apply (apply X (apply k Z)) (apply Y Z)).