NaturalAndLevelDifferent.agda:8,1-26
The argument to BUILTIN LEVEL must be a postulated name
when checking the pragma BUILTIN LEVEL ℕ