∀[n:ℕ]. uiff(upto(n) ~ [];n = 0 ∈ ℤ)
{ ((D 0 THENA Auto) THEN Unfold `upto` 0) }
1. n : ℕ
⊢ uiff([0, n) ~ [];n = 0 ∈ ℤ)