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