MK_COMB_TAC : tactic
SYNOPSIS
Breaks an equality between applications into two equality goals: one for the functions, and other for the arguments.
LIBRARY
bool
STRUCTURE
Tactic
DESCRIPTION
MK_COMB_TAC reduces a goal of the form A ?- f x = g y to the goals A ?- f = g and A ?- x = y. 
    A ?- f x = g y
   ===========================  MK_COMB_TAC
     A ?- f = g,   A ?- x = y

FAILURE
Fails unless the goal is equational, with both sides being applications.
SEEALSO
MK_COMB, AP_TERM, AP_THM, AP_TERM_TAC, AP_THM_TAC
HOL  Kananaskis-13