\doc{Sample proof: useful kinds of axioms}
\p
The axioms in \dflink{set1.lp} fall into several categories:
\begin{description}
\dt \llink{induction-rule}{Induction rules}
\dd 
The first axiom, \f#sort Set generated by {}, insert#, asserts that all
elements of sort \f{S} can be obtained by finitely many applications of
\fq{insert} to \f#{}#.  It provides the basis for defintions and proofs by
induction. 
\p
\dt Explicit definitions
\dd
The second axiom, \f#{e} = insert(e, {})#, is a single \llink{formula} that
defines the operator \f#{__}# (as a constructor for a singleton set).
\p
\dt Inductive definitions
\dd
The next two pairs of axioms provide induction definitions of the membership
operator \f{\in} and the subset operator \f{\subseteq}.  Inductive definitions
generally consist of one formula per generator.
\p
\dt Implicit definitions
\dd
The formula involving the union operator (\f{\union}), together with the other
axioms, completely constrains the interpretation of that operator.
\p
\dt Constraining properties
\dd
The final axiom (that of the extensionality principle) expresses the fact that
if two sets have the same elements, then they must be the same set.
\end{itemize}