fix: `IndPredBelow` should not add auxiliary declarations containing `sorry`

Issue #4535 is being affected by a bug in the structural inductive
predicate termination checker (`IndPred.lean`). This module did not
exist in Lean 3, and it is buggy in Lean 4. In the given example,
it introduces an auxiliary declaration containing a `sorry`, and the
fails. This PR ensures this kind of declaration is not added to the
environment.

Closes #4535

TODO: we need a new maintainer for the `IndPred.lean`.