When applied to a goal A ?- t, the tactic PBETA_TAC produces a new goal
which results from beta-reducing all paired beta-redexes, at any depth, in t.
Variables are renamed where necessary to avoid free variable capture.
A ?- ...((\p. s1) s2)...
========================== PBETA_TAC
A ?- ...(s1[s2/p])...