MK_PAIR
PairRules.MK_PAIR : thm * thm -> thm
Proves equality of pairs constructed from equal components.
When applied to theorems A1 |- a = x and A2 |- b = y, the inference
rule MK_PAIR returns the theorem A1 u A2 |- (a,b) = (x,y).
A1 |- a = x A2 |- b = y
--------------------------- MK_PAIR
A1 u A2 |- (a,b) = (x,y)
Failure
Fails unless both theorems are equational.