Tactics.is_quantified_hypothesis does not reduce anymore to decide whether
a variable is quantified in the goal. This is only used by induction, and
it should be a bad practice to depend on an invisible binder.