\documentclass{article}
\usepackage[margin=0.05in]{geometry}
\usepackage{pslatex}
\usepackage{latexsym}
\begin{document}

\newcommand{\Lazyint}{\mbox{\textit{Lazy Int}}}
\newcommand{\Unit}{\mbox{\textit{Unit}}}
\newcommand{\Int}{\mbox{\textit{Int}}}
\newcommand{\Lazy}[1]{\mbox{\textit{lazy}[\textit{#1}]~}}
\newcommand{\LazyN}{\mbox{\textit{lazy}}~}
\newcommand{\Force}[1]{\mbox{\textit{force}[\textit{#1}]~}}

\noindent
\(
\begin{array}{l@{}l@{}l}
\Sigma;\cdot \vdash & (\lambda y:\Lazyint.\ y + 1) (\lambda x:\Unit.\ e) \leadsto \\
& (\lambda y : \Lazyint. (\Force{\Int} y) + 1)\\
& (\LazyN \lambda x:\Unit.\ e) : \Int
\end{array}
\)

\newpage
\noindent
\(
\begin{array}{l@{}l@{}l}
\Sigma;\cdot \vdash & (\lambda y:\Lazyint.\ y + 1) (\lambda x:\Unit.\ e) \leadsto \\
& (\lambda y : \Lazyint. (\Force{\Int} y) + 1)\\
& (\Lazy{\Int} \lambda x:\Unit.\ m) : \Int
\end{array}
\)

\noindent
where \(
\begin{array}{l@{}l@{}l}
\Sigma;\{x:\Unit\} \vdash e \leadsto m
\end{array}
\)



\end{document}
