AP_TERM_TAC

Tactic.AP_TERM_TAC : tactic

Strips a function application from both sides of an equational goal.

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.

See also

Thm.AP_TERM, Thm.AP_THM, Tactic.AP_THM_TAC, Tactic.MK_COMB_TAC, Tactic.ABS_TAC