\doc{Some sample proofs}

We illustrate how to use LP by presenting some sample proofs along with
explanatory comments.  The proofs show how to derive some basic facts about
finite sets from a simple axiomatization.

\begin{itemize}
\item \dlink{sample_start}{Getting started}
\item \dlink{sample_declare}{Sample declarations} for sorts, operators
\item \dlink{sample_assert}{Sample axioms} for finite sets
\item \dlink{sample_axioms}{Useful kinds of axioms}
\item \dlink{sample_conjectures}{Sample conjectures}
\item \dlink{sample_proof1}{Two easy theorems}
\item \dlink{sample_proof2}{Three theorems} about union
\item \dlink{sample_proof3}{Alternative proofs} of theorems about union
\item \dlink{sample_proof4}{Three theorems} about subset
\item \dlink{sample_proof5}{An alternate induction rule}
\item \dlink{sample_proof6}{Two final theorems} about subset
\item \dlink{sample_guidance}{How to guide a proof}
\end{itemize}