data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ