108 \noindent 

   109 This means we can also assume in this case

   110 

   111 \[

   112 (e)\quad len\,|w_1| \geq len\,|w_2|

   113 \] 

   114 

   115 \noindent 

   116 which is the premise of the rule above.

   117 Instantiating $v_1$ and $v_2$ in the assumptions (b) and (c)

   118 gives us

   119 

   120 \begin{center}

   121 \begin{tabular}{ll}

   122 (b*) & $\vdash Left(w_1) : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\

   123 (c*) & $\vdash Right(w_2) : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\

   124 \end{tabular}

   125 \end{center}

   126 

   127 \noindent Since these are assumptions, we can further analyse

   128 how they could have arisen according to the rules of $\vdash

   129 \_ : \_\,$. This gives us two new assumptions

   130 

   131 \begin{center}

   132 \begin{tabular}{ll}

   133 (b**) & $\vdash w_1 : (der\;c\;r_1) \cdot r_2$\\

   134 (c**) & $\vdash w_2 : der\;c\;r_2$\\

   135 \end{tabular}

   136 \end{center}

   137 

   138 \noindent 

   139 Looking at (b**) we can further analyse how this

   140 judgement could have arisen. This tells us that $w_1$

   141 must have been a sequence, say $u_1\cdot u_2$, with

   142 

   143 \begin{center}

   144 \begin{tabular}{ll}

   145 (b***) & $\vdash u_1 : der\;c\;r_1$\\

   146        & $\vdash u_2 : r_2$\\

   147 \end{tabular}

   148 \end{center}

   149 

   150 \noindent 

   151 Instantiating the goal means we need to prove

   152 

   153 \[

   154 inj\; (r_1 \cdot r_2)\;c\;(Left(u_1\cdot u_2)) \succ_{r_1 \cdot r_2} 

   155 inj\; (r_1 \cdot r_2)\;c\;(Right(w_2))

   156 \]

   157 

   158 \noindent 

   159 We can simplify this according to the rules of $inj$:

   160 

   161 \[

   162 (inj\; r_1\;c\;u_1)\cdot u_2 \succ_{r_1 \cdot r_2} 

   163 (mkeps\;r_1) \cdot (inj\; r_2\;c\;w_2)

   164 \]

   165 

   166 \noindent

   167 This is what we need to prove.

   168 

   169