MK_COMB_TAC

Tactic.MK_COMB_TAC : tactic

Breaks an equality between applications into two equality goals: one for the functions, and other for the arguments.

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.

See also

Thm.MK_COMB, Thm.AP_TERM, Thm.AP_THM, Tactic.AP_TERM_TAC, Tactic.AP_THM_TAC