fix: nontermination when generating the match-expression splitter theorem

This PR fixes a non-termination bug that occurred when generating the
match-expression splitter theorem. The bug was triggered when the
proof automation for the splitter theorem repeatedly applied `injection` to
the same local declaration, as it could not be removed due to forward
dependencies. See issue #6065 for an example that reproduces this
issue.

closes #6065