doc: clarify nondep behaviour

[Vtec234]

This PR clarifies the behaviour of mkLetFVars and family on nondependent ldecls.

Zulip discussion here.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8ce0e045a87ef1259a078eadfce2f81e53706da0 --onto 73422d52fd61c3d5bce6f5edb53c6bd698b1b7ba. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-26 22:27:56)

[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 8ce0e045a87ef1259a078eadfce2f81e53706da0 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-26 22:27:57)