ABS_TAC : tactic
Strips lambda abstraction on both sides of an equation.
When applied to a goal of the form
A ?- (\x. f x) = (\y. g u)
, the tactic
strips away the lambda abstractions:
A ?- (\x. f x) = (\y. g y) =========================== ABS_TAC A ?- f x = g x
Fails unless the goal has the above form, namely an equation both sides of which consist of a lamdba abstraction.