Simplified free_in_context proof

... by moving the appears_free condition as a premise to the conclusion,
since then we can leave all the case splitting to the solver.

Didn't manage to make using_induction_hyp with partially applied IH
work; the --full_context_dependency flag only makes it pre-typecheck,
but then it still fails verification (I have no clue why).