\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{}
\begin{popup}
The truth of $<<1>>3$ depends on $GCD1$, so the correct proof is
\begin{display}
\verb|BY GCD1 DEF Inv, EuclidInv, TypeOK, GCDInv|
\end{display}
\end{popup}
\makepopup