PART_MATCH : (term -> term) -> thm -> term -> thm
PART_MATCH fn (A |- !x1...xn. t) tm
th = |- !x. x ==> x
PART_MATCH (fst o dest_imp) th `T`
|- T ==> T
# num_INDUCTION;; val it : thm = |- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> (!n. P n) # PART_MATCH rand it `!n. n <= n * n`;; val it : thm = |- 0 <= 0 * 0 /\ (!n. n <= n * n ==> SUC n <= SUC n * SUC n) ==> (!n. n <= n * n)
# let th = MESON[num_CASES; NOT_SUC] `(!n. P(SUC n)) <=> !n. ~(n = 0) ==> P n` ... val th : thm = |- (!n. P (SUC n)) <=> (!n. ~(n = 0) ==> P n)
# PART_MATCH lhs th `!n. 1 <= SUC n`;; val it : thm = |- (!n. 1 <= SUC n) <=> (!n. ~(n = 0) ==> 1 <= n)