-∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (inverse (multiply A (multiply B (multiply (multiply (inverse B) C) (inverse (multiply D (multiply A C))))))) D.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
+∀H0:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.eq Univ (inverse (multiply A (multiply B (multiply (multiply (inverse B) C) (inverse (multiply D (multiply A C))))))) D.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3)))