fix: recognize sorts as `Prop` up to universe normalization

This PR fixes a kernel bug: a type whose sort is `Prop` only after universe normalization,
such as `Sort (imax 1 0)`, was not recognized as a proposition, so the kernel allowed a
non-proof field to be projected out of a proof. Such a declaration cannot be written in surface
syntax and can only be produced with metaprogramming, and `nanoda` rejects it.

Because proof irrelevance equates any two proofs of such a type, projecting a `Bool` field out
of two of them gives `false = true`, and hence `False` with no axiom dependencies.
The elaborator blocks this by eagerly normalizing levels.

`type_checker::is_prop` compared `whnf(infer_type(e))` against `Prop` syntactically.
The level `imax 1 0` is definitionally `0`, so a type in `Sort (imax 1 0)` really is a
proposition and proof irrelevance applies to it, but `is_prop` answered `false` and `infer_proj`
therefore skipped its `Prop` restriction. The fix tests the level for zero up to normalization instead.