fix: don't resynthesize unwrapped nested proofs in the grind canonicalizer

[leodemoura]

This PR fixes a grind bug where the canonicalizer could resynthesize a propositional instance (e.g. Nonempty α) occurring in a binder body skipped by preprocessing, producing a closed nested proof lacking the Grind.nestedProof wrapper. Congruence closure then treated the term as distinct from correctly wrapped occurrences of the same application, and grind missed valid contradictions. Closes #13655.

The preprocessing step markNestedSubsingletons wraps every closed nested proof with Grind.nestedProof, but skips forall bodies with loose bound variables; such bodies are re-preprocessed by propagateForallPropUp when instantiated. Resynthesizing an unwrapped proof inside such a body could remove the dependency on the bound variable, and the now-closed body was then internalized via the non-dependent fast path without re-preprocessing. The fix makes canonInst' keep unwrapped Prop-typed instances unchanged in term positions: the forall stays dependent, and the slow path re-preprocesses the instantiated body consistently. Behavior inside types is unchanged, where instances are deliberately unwrapped and resynthesized for structural agreement.

Thanks to @datokrat for the detailed analysis in the issue report.

🤖 Generated with Claude Code

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b9c91298fc961122eadfdf4ff2a3ee4ce6c2071b --onto 79bec6d064d8672cb10864cad3d9fd054b6917ae. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-18 04:55:04)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b9c91298fc961122eadfdf4ff2a3ee4ce6c2071b --onto 79bec6d064d8672cb10864cad3d9fd054b6917ae. You can force reference manual CI using the force-manual-ci label. (2026-07-18 04:55:06)