ABS : term -> thm -> thm
A |- t1 = t2 ------------------------ ABS `x` [Where x is not free in A] A |- (\x.t1) = (\x.t2)
# ABS `m:num` (REFL `m:num`);; val it : thm = |- (\m. m) = (\m. m)