----------------------------------------------------------------------
MK_COMB                                                          (Thm)
----------------------------------------------------------------------
MK_COMB : thm * thm -> thm

SYNOPSIS
Proves equality of combinations constructed from equal
functions and operands.

KEYWORDS
rule, combination, equality.

DESCRIBE
When applied to theorems {A1 |- f = g} and {A2 |- x = y}, the inference
rule {MK_COMB} returns the theorem {A1 u A2 |- f x = g y}.

    A1 |- f = g   A2 |- x = y
   ---------------------------  MK_COMB
       A1 u A2 |- f x = g y




FAILURE
Fails unless both theorems are equational and {f} and {g} are
functions whose domain types are the same as the types of {x} and {y}
respectively.

SEEALSO
Thm.AP_TERM, Thm.AP_THM, Tactic.MK_COMB_TAC.

----------------------------------------------------------------------