\newcommand{\jj}{\justifies}
% \begin{Examplen}
\begin{figure}
\label{fig:strictex}
\prooftree
\[ \mbox{} \jj y \oftp A; \cdot; x  \oftp A \RImp A\RImp B \prv x \hastype A \RImp A\RImp B \using 
Id^1 \]
 \qquad 
\[ \mbox{} \jj  x\oftp A \RImp A\RImp B;\cdot ; y  \oftp A\prv y\hastype A \using Id^1\using \RImp E\]
\justifies
\[
\cdot;\cdot ; x  \oftp A \RImp A\RImp B , y  \oftp A\prv x y^1 \hastype A\RImp B \jj\]
\qquad 
\[\mbox{}\using Id^{u} \jj x \oftpA \RImp A\RImp B, y  \oftp A; \cdot ;\cdot\prv y\hastype A
\using \RImp E\]
\justifies
\[
 \cdot;\cdot; x  \oftp A \RImp A\RImp B ,y\oftp A\prv (x y^1)  y^1 \hastype B
%  \using \RImp I
%  \justifies
%  \[
%  \cdot;\cdot; x  \oftp A \RImp A\RImp B  \prv \l y^1 . (x y^1)  y^1 \hastype A\RImp B
%  \using \RImp I
%  \justifies
% \cdot;\cdot;\cdot\prv \l x^1.\l y^1. (x y^1)  y^1  \hastype (A \RImp A\RImp B)\RImp (A\RImp 
% B)
% \]
% \]
\]
\endprooftree
\caption{First derivation of $(A \RImp A\RImp B)\RImp (A\RImp B)$}
\end{figure}

We now illustrate how the strict application rule 
non-deterministically splits contexts. Consider the typing problem
$\cdot;\cdot; x  \oftp A \RImp A\RImp B ,y\oftp A\prv (x y^1)  y^1 \hastype 
B$. There are four ways to split the strict context:
\[\begin{array}{ll}
\D_{M} = x  \oftp A \RImp A\RImp B ,y\oftp A & \D_{N}=\cdot\\
\D_{M} = x  \oftp A \RImp A\RImp B & \D_{N} = y\oftp A\\
\D_{M} = y\oftp A & \D_{N}= x  \oftp A \RImp A\RImp B\\
\D_{M} =\cdot & \D_{N}=x  \oftp A \RImp A\RImp B ,y\oftp A
\end{array}\]
Only the first two yield a valid derivation (depicted in Fig.~\ref{fig:strictex} 
and Fig.~\ref{fig:strictex2}, as $x$ needs to be strict in the 
leftmost branch.

\begin{figure}
\label{fig:strictex}
\prooftree
\[ \mbox{} \jj y \oftp A; \cdot; x  \oftp A \RImp A\RImp B \prv x \hastype A \RImp A\RImp B \using 
Id^1 \]
 \qquad 
\[ \mbox{} \jj  x\oftp A \RImp A\RImp B,y  \oftp A;\cdot ; \cdot\prv y\hastype 
A \using Id^u\using \RImp E\]
\justifies
\[
 y  \oftp A;\cdot ; x  \oftp A \RImp A\RImp B \prv x y^1 \hastype A\RImp B \jj\]
\qquad 
\[\mbox{}\using Id^1 \jj x \oftpA \RImp A\RImp B; \cdot ; y  \oftp A\prv y\hastype A
\using \RImp E\]
\justifies
\[
 \cdot;\cdot; x  \oftp A \RImp A\RImp B ,y\oftp A\prv (x y^1)  y^1 \hastype B
%  \using \RImp I
%  \justifies
%  \[
%  \cdot;\cdot; x  \oftp A \RImp A\RImp B  \prv \l y^1 . (x y^1)  y^1 \hastype A\RImp B
%  \using \RImp I
%  \justifies
% \cdot;\cdot;\cdot\prv \l x^1.\l y^1. (x y^1)  y^1  \hastype (A \RImp A\RImp B)\RImp (A\RImp 
% B)
% \]
% \]
\]
\endprooftree
\caption{Second derivation of $(A \RImp A\RImp B)\RImp (A\RImp B)$}
\end{figure}
