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