chore: collectForwardDeps returns only free variables, not metavars

[JovanGerb]

This PR removes some unreachable code that acts as if collectForwardDeps could return metavariables. This confusing code was first added in commit 50ae170. And then to explain this, in #1625 it was explicitly documented that collectForwardDeps could return metavariables.

So I removed the metavariable handling in the functions that are only run on the result of collectForwardDeps.

It may also be a bug that no metavariables can reach this code, but in that case there should be a TODO.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6088 has successfully built against this PR. (2024-11-15 12:37:26) View Log
• ✅ Mathlib branch lean-pr-testing-6088 has successfully built against this PR. (2024-11-24 22:47:38) View Log

[nomeata]

I’ll leave others to review this (but looks good if it’s really dead code). Could you maybe leave assert! x.isVar statements in place, so that the next time someone reads the code they benefit from your findings, and we notices when they are violated?

[JovanGerb]

Ok, I've added assert! toRevert.all (·.isFVar) for the result of collectForwardDeps, which is the the array passed to the other functions. (although I don't this this is reaally necessary, since otherwise there would be a panic from Expr.fvarId!)