fix: reject declarations naming the kernel's `_nested` auxiliary types

This PR fixes a kernel bug: an inductive declaration could name 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.

`environment::add_inductive` 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.