\documentclass{article}

\usepackage{pf}
\usepackage{html}

%\pfhidelevel{1}

\newcommand{\N}{{\bf N}}
\newcommand{\Q}{{\bf Q}}
\newcommand{\Z}{{\bf Z}}

\newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}}

%% Set \stepsep for proofs according to level.
\makefcn{\mylevelsep}{.3em}{{.3em}{.1em}{0pt}}
\renewcommand{\stepsep}{\mylevelsep{\pfLevelCount}}

\title{Proof that all natural numbers are interesting}
\author{Leslie Lamport}
\date{December 1, 1993}
\begin{document}
\maketitle

\begin{abstract}
\noindent \latexhtml{Printable}{HTML} version of a sample
\htmladdnormallink{proof}{http://foldoc.doc.ic.ac.uk/foldoc/foldoc.cgi?proof}
that uses
\htmladdnormallink{Lamport's}{http://www.lamport.org/}
\htmladdnormallink{\latex}{http://www.latex-project.org/} \htmladdnormallink{proof
style}{http://research.microsoft.com/users/lamport/latex/pf.sty}
\cite{Lamport1993}, illustrating how structured proofs can be
converted to \htmladdnormallink{HTML}{http://foldoc.doc.ic.ac.uk/foldoc/foldoc.cgi?html} pages via \htmladdnormallink{\latextohtml}{http://www.latex2html.org/} enriched with
\htmladdnormallink{extensions for Lamport's proof
style}{http://www.dbai.tuwien.ac.at/proj/pf2html/}.
\end{abstract}

\bigskip

\noindent {\bf Theorem} \ All natural numbers are interesting.
\assume{$n$ a natural number.}
\prove{$n$ is interesting.}
\begin{proof}
\step{1}{A number is interesting if it is the smallest number not in
         an interesting set.}
  \begin{proof}
    \pf\ By definition of interesting.
  \end{proof}
\step{2}{\case{$n=0$}}
  \begin{proof}
  \pf\ By \stepref{1}, since $0$ is the smallest natural number not in
    $\emptyset$.
  \end{proof}
\step{3}{\case{\begin{enumerate}
                 \item $n>0$
                 \item $n-1$ is  interesting
               \end{enumerate}}}
  \begin{proof}
   \pf\ By \stepref{1}, since case assumption \levelref{3}
   implies that $\{k : k \leq n-1\}$ is interesting.
%    since the set of all numbers not greater than
%    an interesting number is interesting.
  \end{proof}
\qedstep
\begin{proof}
\pf\ Steps \stepref{2} and \stepref{3}, assumption \pflevelnumber{0}{},
 and mathematical induction.
\end{proof}
\end{proof}

\begin{thebibliography}{}
\bibitem{Lamport1993} Leslie Lamport, 1993, How to write a proof. In
{\em Global Analysis of Modern Mathematics}, pp.\ 311--321. Publish or
Perish, Houston, Texas, February 1993.  A symposium in honor of
Richard Palais' sixtieth birthday (also published as SRC Research
Report 94).
\htmladdnormallink{http://research.microsoft.com/users/lamport/proofs/src94.ps.Z}{http://research.microsoft.com/users/lamport/proofs/src94.ps.Z}
\end{thebibliography}

\end{document}