AP_TERM_TAC : tactic
SYNOPSIS
Strips a function application from both sides of an equational goal.
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 CONDITIONS
Fails unless the goal is equational, with both sides being applications of the same function.
SEE ALSO
ABS_TAC
,
AP_TERM
,
AP_THM_TAC
,
BINOP_TAC
,
MK_COMB_TAC
.