Any good way to write mathematical induction proof steps in LaTeX?

I think this is a work for the alignat. Some comments about the code:

• The package enumitem provides the label key which I have used to modify the label for the inner itemize environment.

• I have manually added some space (v. \medskip in the code) so that the output resembles the scan copy.

  \documentclass{amsart} % http://www.ctan.org/pkg/amsart
  \usepackage{enumitem}  % http://www.ctan.org/pkg/enumitem
  \begin{document}
  \begin{itemize}
  \item \emph{Induction Principle}: The formula $\phi$ may be derived by proving the formula \medskip
  \begin{itemize}[label=$\lozenge$, itemsep=2ex]
  \item \emph{Base Case}:
  \[\texttt{(implies (and (not }q_1 \texttt{)} \dots \texttt{(not }q_k\texttt{)) }\phi\texttt{)}\]
  \item \emph{Induction Step(s)}: For each $1 \leq i \leq n$,   
  \begin{alignat*}{5}
  \texttt{(implies} &\quad&&\texttt{(and} &\quad& &&q_i \\
                    &&     &              &&      &&\phi/\sigma_{i,1}\\
                    &&     &              &&      &&\dots\\
                    &&     &              &&      &&\phi/\sigma_{i,k_i}\texttt{)} \\
                    &&     &\phi\texttt{)}
  \end{alignat*}
  provided that for terms $m, q_1, \dots, q_k$, and substitutions $\sigma_{i,j}$ ($1 \leq i \leq h_i$), the following measure conjectures are theorems.
  \item \texttt{(EO-ORDINALP} $m$\texttt{)}
  \item For each $1 \leq i \leq k$ and for $1 \leq j \leq h_i$, 
  \[\texttt{(IMPLIES } q_i \texttt{ (EO-ORD-< } m/\sigma_{i,j} \quad m \texttt{))}\]
  \end{itemize}
  \end{itemize}
  \end{document}
  

Thanks to egreg who has kindly gifted me these and agreed not to steal my green tick, I have learnt atleast two different ways of doing this:

• a quick reference for tabbing could be this one.

• There is one other important fact that he told me here: If a minipage contains only a tabbing environment, the minimum of width of the tabbing environment and the specified width would be the width of the minipage.

The Code Snippets

\[ % works without \[ and \] as well.
\begin{minipage}{\linewidth}
\begin{tabbing}
\texttt{(implies}\quad\= \texttt{(and}\quad\= $q_i$ \\
                      \>                   \> $\phi/\sigma_{i,1}$\\
                      \>                   \> \dots\\
                      \>                   \>  $\phi/\sigma_{i,k_i}$\texttt{)} \\
                      \> $\phi$\texttt{)}
\end{tabbing}
\end{minipage}
\] 

\[ % works without \[ and \] as well.
\begin{minipage}{\linewidth}\ttfamily
\begin{tabbing}
(implies\quad\= (and\quad\= $q_i$ \\
             \>          \> $\phi/\sigma_{i,1}$\\
             \>          \> \dots\\
             \>          \>  $\phi/\sigma_{i,k_i}$) \\
             \> $\phi$)
\end{tabbing}
\end{minipage}
\]

Please note that, I have added the comment:

 % works without \[ and \] as well. 

to bring to the fore that, you may therefore align this to the left, as in the scan by dropping the \[...\].

What I do is just to use a description environment, with Base: and Induction: labels.