22 

    25 text {*

    26   Things to include at the end:

    27 

    28   \begin{itemize}

    29   \item say something about add-inductive-i to return

    30   the rules

    31   \item say that the induction principle is weaker (weaker than

    32   what the standard inductive package generates)

    33   \end{itemize}

    34   

    35 *}

    36 

    37