∀H0:eq Univ (multiply c b) identity.
∀H1:∀X:Univ.eq Univ (multiply (inverse X) X) identity.
∀H2:∀X:Univ.eq Univ (multiply identity X) X.
∀H0:eq Univ (multiply c b) identity.
∀H1:∀X:Univ.eq Univ (multiply (inverse X) X) identity.
∀H2:∀X:Univ.eq Univ (multiply identity X) X.