fix: queue structure eta equations in `grind` internalization

This PR fixes an internal `grind` error ("term has not been internalized") caused by structure eta.

When internalizing a structure-valued term `a`, `propagateEtaStruct` internalized `⟨a.1, ..., a.n⟩` eagerly. If `a` is the argument of a projection `a.i` that is still being internalized (e.g., `a := g y` while internalizing `(g y).val`), this term contains the incomplete application `a.i`, and the solver hooks receive it with missing arguments. The fix adds `ToProcessElement.internalizeRhsAddEq` and uses it to queue the eta equation until no application is in progress.

Closes #16101

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>