\doc{Sample proofs: useful kinds of axioms}
\p
The axioms in \dflink{set1.lp}{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 definitions and proofs by
induction. 
\p
\dt Explicit definitions
\dd
The second axiom, \f#{e} = insert(e, {})#, is a single \llink{formula}{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 final formula, \f{e \in (x \union y) <=> e \in x \/ e \in y}, in the first
\fq{assert} command, together with the other axioms, completely constrains the 
interpretation of the \fq{\union} operator.
\p
\dt Constraining properties
\dd
The second \fq{assert} command formalizes the 
\def{principle of extensionality}, which asserts that any two sets with exactly
the same elements must be the same set.
\end{description}