AP_TERM : term -> thm -> thm
A |- x = y ---------------- AP_TERM `f` A |- f x = f y
# NUM_ADD_CONV `2 + 2`;; val it : thm = |- 2 + 2 = 4 # AP_TERM `(+) 1` it;; val it : thm = |- 1 + 2 + 2 = 1 + 4