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