When applied to a goal A ?- !x. t, the tactic GEN_TAC reduces it to
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
A ?- t[x'/x]