∀v:Univ.
∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply v X) Y) Z) (apply (apply Z X) Y).
∀H1:∀X:Univ.eq Univ (apply m X) (apply X X).
∀v:Univ.
∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (apply (apply (apply v X) Y) Z) (apply (apply Z X) Y).
∀H1:∀X:Univ.eq Univ (apply m X) (apply X X).