fix: bug in gen_injective_theorems%

[digama0]

In the example

inductive WF : Nat → Type 1
  | mk (α : Type) (fn : α → Nat) (arg : α) : WF (fn arg)

the implementation was treating fn and arg as fixed because they appear in the target type, but not α because it is not in the target type, leading to a type error because the type of fn depends on α. Now we take the transitive closure of the variables in the target type under the backward dependency relation.

Surprisingly there was not a function which does this backward dependency calculation (it is implemented in bits and pieces scattered around, and forward dependency has a function for it but not backward dependency) so I exposed a function to do it as part of CollectFVars.