Breaks down a goal between function applications into equality of functions and
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
A ?- f = g A ?- x = y
Fails if the conclusion of the goal is not an equation between applications.