chore: check the structure name when comparing projections in the kernel

This PR makes the kernel compare the structure name when deciding
whether two projection expressions are definitionally equal.
Both `type_checker::is_def_eq_core` and `equiv_manager::is_equiv_core`
compared only the projection index and the projected expression,
ignoring `proj_sname`.

This is not an exploitable bug: every projection in a submitted
declaration passes through `infer_proj`, which rejects a structure name
that does not match the projected expression's type, and projections
constructed by the kernel during reduction always carry the correct
name. So two projections reaching def-eq can only disagree on the
structure name if one of them is ill-typed. The check turns that
global invariant into a local one: after #14577 closed the
nested-inductive path that let unchecked projections into the
environment (#14576), these comparisons were the remaining places
where a future injection bug could have been amplified into a def-eq
attack surface.

There is no completeness loss for well-typed terms, since
identical projected expressions force identical structure names.