When applied to a term s and a goal A ?- !x. t, the tactic FILTER_GEN_TAC
fails if the quantified variable x is the same as s, but otherwise
advances the goal in the same way as GEN_TAC, i.e. returns the goal
A ?- t[x'/x] where x' is a variant of x chosen to avoid clashing with
any variables free in the goal’s assumption list. Normally x' is just x.
A ?- !x. t
============== FILTER_GEN_TAC "s"
A ?- t[x'/x]