NUM_MIN_CONV : term -> thm
|- MIN m n = s
# NUM_MIN_CONV `MIN 11 12`;; val it : thm = |- MIN 11 12 = 12