∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply X (multiply Y (multiply Y Y))) (multiply 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 (multiply Y Y))) (multiply 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 (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a b))))))))))))))))) (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b (multiply b (multiply b (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 (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a (multiply b (multiply a b))))))))))))))))) (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply a (multiply b (multiply b (multiply b (multiply b (multiply b (multiply b (multiply b (multiply b b))))))))))))))))))