CoinductiveBuiltinNatural.agda:11,21-24
ℕ !=< ∞ ℕ of type Set
when checking that the expression suc has type ℕ → ℕ