∀a:Univ.
∀b:Univ.
∀c:Univ.
∀difference:∀_:Univ.∀_:Univ.Univ.
∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (difference (difference X Y) Z) (difference (difference X Z) Y).
∀H1:∀X:Univ.∀Y:Univ.eq Univ (difference X (difference X Y)) (difference Y (difference Y X)).
∀a:Univ.
∀b:Univ.
∀c:Univ.
∀difference:∀_:Univ.∀_:Univ.Univ.
∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (difference (difference X Y) Z) (difference (difference X Z) Y).
∀H1:∀X:Univ.∀Y:Univ.eq Univ (difference X (difference X Y)) (difference Y (difference Y X)).