perf: skip redundant nested proof abstraction for smart unfolding definitions

This PR removes a redundant `abstractNestedProofs` pass when elaborating structurally recursive definitions, which reduces elaboration time for files with many such definitions.

`structuralRecursion` abstracts the nested proofs of the original definition body before registering it for equation lemma generation, and then passes the result to `addSmartUnfoldingDef`. The latter calls `addNonRec`, which abstracted the nested proofs again even though the term no longer contains any. `addNonRec` now takes an `abstractProofs` flag, and `addSmartUnfoldingDef` sets it to `false`.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>