∀H0:∀A:Univ.eq Univ identity (divide A A).
∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).
∀H0:∀A:Univ.eq Univ identity (divide A A).
∀H1:∀A:Univ.eq Univ (inverse A) (divide identity A).
∀H2:∀A:Univ.∀B:Univ.eq Univ (multiply A B) (divide A (divide identity B)).