fix: reject declarations naming the kernel's `_nested` auxiliary types (#14616)

This PR fixes a kernel bug: an inductive declaration could reference one
of the auxiliary types the kernel generates when eliminating nested
inductives, and end up with a stored constructor type that is ill typed.
Such a declaration can only be produced with metaprogramming.

The auxiliary types live under `_nested` and exist only in the temporary
environment used for the elimination. A constructor naming one is
checked there, but `restore_nested` then rewrites the name back to the
nested type, which can live in a different universe. Combined with proof
irrelevance, the resulting ill-typed constructor makes two distinct
functions look like proofs of the same proposition, and `equiv_manager`
closes them transitively, giving `False` with no axiom dependencies.

The kernel now rejects the reserved prefix, alongside the existing
checks for metavariables and free variables. Both `Expr.const` names and
`Expr.proj` structure names are covered: the kernel rewrites nested
occurrences in the constructor to the auxiliary type, so a projection
can reach that type without the declaration naming it as a constant.