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