MK_COMB_TAC : tactic

SYNOPSIS

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.