∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply (add (multiply X Y) X) (add X Y)) X.
∀H3:∀X:Univ.∀Y:Univ.eq Univ (multiply (add X Y) (add X (inverse Y))) X.
∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (add (multiply X Y) (multiply Y Z)) Y) Y.
∀H2:∀X:Univ.∀Y:Univ.eq Univ (multiply (add (multiply X Y) X) (add X Y)) X.
∀H3:∀X:Univ.∀Y:Univ.eq Univ (multiply (add X Y) (add X (inverse Y))) X.
∀H4:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (add (multiply X Y) (multiply Y Z)) Y) Y.