1. x : ℤ
2. [y] : ℕ
3. |x| = y ∈ ℤ
⊢ (x = y ∈ ℤ) ∨ (x = (-y) ∈ ℤ)
{ (RWO "absval_unfold2" (-1) THENA Auto) }
3. if (0) < (x) then x else (-x) = y ∈ ℤ