AP_TERM_TAC : tactic
SYNOPSIS
Strips a function application from both sides of an equational goal.
LIBRARY
bool
STRUCTURE
Tactic
DESCRIPTION
AP_TERM_TAC reduces a goal of the form A ?- f x = f y by stripping away the function applications, giving the new goal A ?- x = y. 
    A ?- f x = f y
   ================  AP_TERM_TAC
     A ?- x = y

FAILURE
Fails unless the goal is equational, with both sides being applications of the same function.
SEEALSO
AP_TERM, AP_THM, AP_THM_TAC, MK_COMB_TAC, ABS_TAC
HOL  Kananaskis-13