MK_ABS
Drule.MK_ABS : (thm -> thm)
Abstracts both sides of an equation.
When applied to a theorem A |- !x. t1 = t2, whose conclusion is a
universally quantified equation, MK_ABS returns the theorem
A |- \x. t1 = \x. t2.
A |- !x. t1 = t2
-------------------------- MK_ABS
A |- (\x. t1) = (\x. t2)
Failure
Fails unless the theorem is a (singly) universally quantified equation.