∀apply:∀_:Univ.∀_:Univ.Univ.
∀combinator:Univ.
∀s:Univ.
∀w:Univ.
∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply w X) Y) (apply (apply X Y) Y).
∀apply:∀_:Univ.∀_:Univ.Univ.
∀combinator:Univ.
∀s:Univ.
∀w:Univ.
∀H0:∀X:Univ.∀Y:Univ.eq Univ (apply (apply w X) Y) (apply (apply X Y) Y).