\doc{Subgoals}
\ref{subgoals}

A \def{subgoal} is a conjecture introduced by a method of
\dlink{../proof/backward}{backward inference} in an attempt to prove another
conjecture.  Often additional hypotheses may be used in the proof of the
subgoal.