\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{Hint}
\begin{popup}
\subsection*{Hint}

Remember that you must show that adding or removing stuttering steps
to/from a behavior $\sigma$ does not change whether or not $WF_{vars}(A)$
is true of $\sigma$.  Adding or removing stuttering steps does not
include the meaningless possibility of adding or removing an infinite
sequence of stuttering steps in the middle of a behavior.  You need
not consider the possibility of removing an infinite sequence of
stuttering steps from the end of a behavior, since that does not
produce a behavior (which must be infinite).

\end{popup}
\makepopup