\newcommand{\jj}{\justifies}
\newcommand{\aaa}{y \oftp A; \cdot; x  \oftp A \RImp A\RImp B \prv x
\hastype A \RImp A\RImp }
\newcommand{\bbb}{x\oftp A \RImp A\RImp B;\cdot ; y  \oftp A\prv
 y\hastype A }
\newcommand{\ccc}{\cdot;\cdot ;( x  \oftp A \RImp A\RImp B , y  \oftp
  A)\prv x y^1 \hastype A\RImp B}
\newcommand{\ddd}{ (x \oftp A \RImp A\RImp B, y  \oftp A); \cdot
  ;\cdot\prv y\hastype A}
\newcommand{\eee}{ \cdot;\cdot; (x  \oftp A \RImp A\RImp B ,y\oftp
  A)\prv (x y^1)  y^1 \hastype B}


% \prooftree
% \[ \mbox{} \jj\aaa \using Id^1 \]
%  \qquad 
% \[ \mbox{} \jj  \bbb\using Id^1
% \using \RImp E\]
% \justifies
% \[
% \ccc \jj\]
% \qquad 
% \[\mbox{}\using Id^{u} \jj\ddd
% \using \RImp E\]
% \justifies
% \[
% \eee
% \]
% \endprooftree
% \prooftree
% %\[ \mbox{} \jj A \using Id^1 \]
%  \qquad 
% %\[ \mbox{} \jj  B\using Id^1\] \using \RImp E\]
% %\justifies
% \[
% C \jj D

% %\qquad 
% %\[\mbox{}\using Id^{u} \jj D\]
% %\using \RImp E
% %\justifies
% %\[
% %E
% \]
% \endprooftree
$$
\prooftree
\[
\[ \mbox{} \jj \aaa\using Id^1\]
\quad 
\[ \mbox{} \jj \bbb\using Id^1\]
\jj \ccc\using \RImp E\]
\quad
\[ \mbox{} \jj \ddd\using Id^u\]
\jj
\eee\using \RImp E
\endprooftree
$$

$$

$$

\end{document}

\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 \oftp A \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  $\cdot;\cdot; (x  \oftp A \RImp A\RImp B ,y\oftp A)\prv (x y^1)  y^1\hastype B$}
\end{figure}
