Strips an abstraction from each side of an equational goal.
DESCRIPTION
ABS_TAC reduces a goal of the form A ?- (\x. s[x]) = (\y. t[y])
by stripping away the abstractions to give a new goal A ?- s[x'] = t[x']
where x' is a variant of x, the bound variable on the left-hand side,
chosen not to be free in the current goal's assumptions or conclusion.
A ?- (\x. s[x]) = (\y. t[y])
================================ ABS_TAC
A ?- s[x'] = t[x']
FAILURE CONDITIONS
Fails unless the goal is equational, with both sides being abstractions.