Applies a tactic to one goal, referenced by number, in the current goal list,
replacing that goal with the resulting subgoals.
DESCRIPTION
enth tac i applies tac to all the i’th goal in the current goal list,
replacing that goal in the goal list with the subgoals produced by tac.
It is an abbreviation for expand_list (NTH_GOAL tac i).
USES
For interactively constructing suitable compound tactics,
for example to test whether a particular subgoal can be proved easily,
before attacking the other subgoals.