∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply X (multiply Y Y)) (multiply Y (multiply Y X)).
∀a:Univ.
∀b:Univ.
∀multiply:∀_:Univ.∀_:Univ.Univ.
∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply X (multiply Y Y)) (multiply Y (multiply Y X)).
-∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).eq Univ (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a b))))))) (multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b b)))))))
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).eq Univ (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a b))))))) (multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b b))))))))