INSTANTIATE : instantiation -> thm -> thm
# let t = lhs(concl(SPEC_ALL NOT_FORALL_THM));; val t : term = `~(!x. P x)` # let i = term_match [] t `~(!n. prime(n) ==> ODD(n))`;; val i : instantiation = ([(1, `P`)], [(`\n. prime n ==> ODD n`, `P`)], [(`:num`, `:A`)]) # INSTANTIATE i (SPEC_ALL NOT_FORALL_THM);; val it : thm = |- ~(!x. prime x ==> ODD x) <=> (?x. ~(prime x ==> ODD x))