Breaks down a goal between function applications into equality of functions and
arguments.
DESCRIPTION
Given a goal whose conclusion is an equation between function applications
A ?- f x = g y, the tactic MK_COMB_TAC breaks it down to two subgoals
expressing equality of the corresponding rators and rands:
A ?- f x = g y
================================ MK_COMB_TAC
A ?- f = g A ?- x = y
FAILURE CONDITIONS
Fails if the conclusion of the goal is not an equation between applications.