∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply (inverse Y) Y X) X.
∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply X X Y) X.
∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply Y X X) X.
∀H0:∀X:Univ.∀Y:Univ.eq Univ (multiply (inverse Y) Y X) X.
∀H1:∀X:Univ.∀Y:Univ.eq Univ (multiply X X Y) X.
∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply Y X X) X.
-∀H3:∀V:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply V W X) Y (multiply V W Z)) (multiply V W (multiply X Y Z)).eq Univ (multiply a (inverse a) b) b
+∀H3:∀V:Univ.∀W:Univ.∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (multiply (multiply V W X) Y (multiply V W Z)) (multiply V W (multiply X Y Z)).eq Univ (multiply a (inverse a) b) b)