\documentclass[letterpaper]{article}
\usepackage{fullpage,theorem,proof,prooftree,amssymb,url}

\newcommand{\answer}[1]{\begin{solution} #1 \end{solution}}

\newcommand{\cf}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\rn}[1]{\textsc{#1}}

\theoremstyle{margin}
\theorembodyfont{\rmfamily}
\newtheorem{exercise}{Exercise}
\newtheorem{solution}{Solution}

\begin{document}

\begin{exercise}
Show the derivations of the following typing judgments:
\begin{enumerate}
\item \cf{if\ false\ then\ 0\ else\ succ\ 0 : Nat}
\item \cf{succ\ (if\ iszero\ 0\ then\ succ\  0\  else\  pred\  0) : Nat}
\end{enumerate}
\end{exercise}

\answer{This solution uses the \cf{prooftree} package.
\begin{enumerate}

   \item \prooftree
            % 1
            \prooftree
            \justifies \cf{false : Bool}
            \using \rn{T-False}
            \endprooftree
            \quad
            % 2
            \prooftree
            \justifies \cf{0 : Nat}
            \using \rn{T-Zero}
            \endprooftree
            \quad
            % 3
            \prooftree
               \prooftree
               \justifies \cf{0 : Nat}
               \using \rn{T-Zero}
               \endprooftree
            \justifies \cf{succ\ 0 : Nat}
            \using \rn{T-Succ}
            \endprooftree
         \justifies \cf{if\ false\ then\ 0\ else\ succ\ 0 : Nat}
         \using \rn{T-If}
         \endprooftree
         \vspace{1.5em}

   \item \prooftree
            \prooftree
               \prooftree
                  \prooftree \justifies \cf{0 : Nat} \using \rn{T-Zero} \endprooftree
               \justifies \cf{iszero\ 0 : Bool}
               \using \rn{T-IsZero}
               \endprooftree
               \quad
               \prooftree
                  \prooftree \justifies \cf{0 : Nat} \using \rn{T-Zero} \endprooftree
               \justifies \cf{succ\ 0 : Nat}
               \using \rn{T-Succ}
               \endprooftree
               \quad
               \prooftree
                  \prooftree \justifies \cf{0 : Nat} \using \rn{T-Zero} \endprooftree
               \justifies \cf{pred\ 0 : Nat}
               \using \rn{T-Pred}
               \endprooftree
            \justifies \cf{if\ iszero\ 0\ then\ succ\  0\  else\ pred\  0 : Nat}
            \using \rn{T-If}
            \endprooftree
         \justifies \cf{succ\ (if\ iszero\ 0\ then\ succ\  0\  else\  pred\ 0) : Nat}
         \using \rn{T-Succ}
         \endprooftree

\end{enumerate}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\noindent
\rule{\textwidth}{2pt}

\begin{exercise}
Show the derivations of the following typing judgments:
\begin{enumerate}
\item \cf{if\ false\ then\ 0\ else\ succ\ 0 : Nat}
\end{enumerate}
\end{exercise}

\answer{This solution uses the \cf{proof} package.  \begin{enumerate}

\item
\[
\infer[\rn{T-If}]
  {\cf{if\ false\ then\ 0\ else\ succ\ 0 : Nat}}
  {% 1
   % 2
   \infer[\rn{T-False}]
    {\cf{false : Bool}}
    {}
   &
   \infer[\rn{T-Zero}]
    {\cf{0 : Nat}}
    {}
   % 3
   &
   \infer[\rn{T-Succ}]
    {\cf{succ\ 0 : Nat}}
    {\infer[\rn{T-Zero}]
      {\cf{0 : Nat}}
      {}
    }
  }
\]

\end{enumerate}
}

\end{document}