The function top_goal is part of the subgoal package. It returns the top goal
of the goal stack in the current proof state. For a description of the subgoal
package, see set_goal.
FAILURE CONDITIONS
A call to top_goal will fail if there are no unproven goals. This could be
because no goal has been set using set_goal or because the last goal set has
been completely proved.