fix: IndPred: track function's motive in a let binding, use withoutProofIrrelevance, no chaining

[nomeata]

This is a variant of #4827, mostly to improve my understanding.

When replacing recursive calls by the corresponding induction hypothesis, it replaces the use of IndPredBelow.backwardsChaining with a non-recursive search through the local context. I want to see if this works as well, or if the chaining is strictly necessary. The corresponding code in brecOn doesn’t need such recursive calls, so I am optimistic.

(PR description will be updated should this or a variant of it find the way to master.)