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