ABS_TAC
Tactic.ABS_TAC : tactic
Strips lambda abstraction on both sides of an equation.
When applied to a goal of the form A ?- (\x. M) = (\y. N) (where M
and N may or may not mention their respective bound variables), the
tactic ABS_TAC strips away the lambda abstractions:
A ?- (\x. f x) = (\y. g y)
============================ ABS_TAC
A ?- f x = g x
Failure
Fails unless the goal has the above form, namely an equation both sides of which consist of a lamdba abstraction.
Comments
When the lambda abstractions' bound variables conflict with existing free variables in the goal, variants of those names may occur in the goal that results.