∀[a,b:ℕ].  (a = b ∈ ℤ) supposing ((b | a) and (a | b)){ (UnivCD THENA Auto) }1. a : ℕ2. b : ℕ3. a | b4. b | a⊢ a = b ∈ ℤ