AP_THM_TAC : tactic
Strips identical operands from functions on both sides of an equation.
When applied to a goal of the form
A ?- f x = g x
, the tactic
strips away the operands of the function application:
A ?- f x = g x ================ AP_THM_TAC A ?- f = g
Fails unless the goal has the above form, namely an equation both sides of which consist of function applications to the same argument.