-∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Y (multiply (multiply Y (multiply (multiply Y Y) (multiply X Z))) (multiply Z (multiply Z Z)))) X.eq Univ (multiply a (multiply a (multiply a a))) identity
+∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply Y (multiply (multiply Y (multiply (multiply Y Y) (multiply X Z))) (multiply Z (multiply Z Z)))) X.eq Univ (multiply a (multiply a (multiply a a))) identity)