\begin{proof}
  \begin{induction}{typing-decl}
    \case{WfAtom}
    \case{WfVar}
    \case{PropSet}
    \case{Type}
    \case{Var}
    \case{Prod}
    \case{Abs}
    \case{App}
    \case{LetIn}
    \case{Sigma}
    \case{Sum}
    \case{LetSum}
    \case{Subset}
    \case{Subsum}
  \end{induction} 
\end{proof}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "subset-typing"
%%% LaTeX-command: "TEXINPUTS=\"style:$TEXINPUTS\" latex"
%%% End: