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