MK_COMB : thm * thm -> thm

- STRUCTURE
- SYNOPSIS
- Proves equality of combinations constructed from equal functions and operands.
- DESCRIPTION
- 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

HOL Kananaskis-14