MK_COMB
Thm.MK_COMB : thm * thm -> thm
Proves equality of combinations constructed from equal functions and operands.
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.