EXPAND_TAC : string -> tactic
val it : goalstack = 1 subgoal (1 total) 0 [`12345 + 12345 = n`] `n + f n = f n`
# e(EXPAND_TAC "n");; val it : goalstack = 1 subgoal (1 total) 0 [`12345 + 12345 = n`] `(12345 + 12345) + f (12345 + 12345) = f (12345 + 12345)`