refactor: IndPredBelow: use `apply_assumption`

[nomeata]

when transforming the match statements in IndPredBelow, given a local variable x : T, we need to search for hx : T.below x. Previously this was done using the custom backwardsChaining method, although my hypothesis is that we don’t need to chain anything here, and can use apply_assumption.