fix: recognize sorts as `Prop` up to universe normalization (#14613)

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.