fix: make the kernel `is_prop` check require a sort

This PR fixes a soundness issue.

**TL;DR.** The kernel's `is_prop` decided whether a term is a proposition by taking the weak head normal form of its inferred type and checking that the result is syntactically `Sort 0`. When the inferred type did not reduce to a sort but was left as a stuck term, `is_prop` returned `false` instead of treating the term as ill-formed. This let the proof-irrelevance guard in projection inference be skipped, so a non-proof field could be projected out of a value used as a `Prop`, and `False` derived. The fix computes the inferred type with `ensure_sort`, which reduces it and requires the result to be a sort, raising `(kernel) type expected` otherwise. The bogus proof was also accepted by nanoda, an independent implementation of the Lean kernel.

When a field is projected out of a value whose type is a proposition, the kernel requires the field's type to also be a proposition. This is what keeps proof irrelevance sound: any two proofs of the same proposition are definitionally equal, so if a projection could read a piece of data (something not itself a proof) out of a proof, that data would be forced to be equal for all proofs, which is false in general. The guard is expressed in terms of `is_prop`.

`is_prop e` computed `whnf (infer_type e)` and returned whether the result is a sort whose level normalizes to zero. The problem is the case where `infer_type e` is a stuck term that does not reduce to a sort, for example an `Eq.rec` whose major premise is a free variable. There `whnf` returns the stuck term, `is_sort` is `false`, and `is_prop` returns `false`. Returning `false` means "not a proposition", which skips the projection guard even when the value is being used as a `Prop` elsewhere. With the guard skipped, a data field can be projected out of that value, and combined with proof irrelevance this yields `False`.

The fix replaces `whnf` with `ensure_sort`: `is_prop` now reduces the inferred type and requires it to be a sort, raising `(kernel) type expected` if it is not. A value whose type does not reduce to a sort is ill-formed, so rejecting it is correct. On well-typed terms the type of a type is always a genuine sort, so the stricter check never fires spuriously.

The bogus proof was also accepted by nanoda, an independent implementation of the Lean kernel.