diff -r 5bc72d6d633d -r 7093e600ec2c thys/notes.tex
--- a/thys/notes.tex	Thu Jan 29 23:42:44 2015 +0000
+++ b/thys/notes.tex	Fri Jan 30 11:42:53 2015 +0000
@@ -105,6 +105,68 @@
 \end{tabular}
 \end{center}
 
+\noindent 
+This means we can also assume in this case
+
+\[
+(e)\quad len\,|w_1| \geq len\,|w_2|
+\] 
+
+\noindent 
+which is the premise of the rule above.
+Instantiating $v_1$ and $v_2$ in the assumptions (b) and (c)
+gives us
+
+\begin{center}
+\begin{tabular}{ll}
+(b*) & $\vdash Left(w_1) : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\
+(c*) & $\vdash Right(w_2) : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\
+\end{tabular}
+\end{center}
+
+\noindent Since these are assumptions, we can further analyse
+how they could have arisen according to the rules of $\vdash
+\_ : \_\,$. This gives us two new assumptions
+
+\begin{center}
+\begin{tabular}{ll}
+(b**) & $\vdash w_1 : (der\;c\;r_1) \cdot r_2$\\
+(c**) & $\vdash w_2 : der\;c\;r_2$\\
+\end{tabular}
+\end{center}
+
+\noindent 
+Looking at (b**) we can further analyse how this
+judgement could have arisen. This tells us that $w_1$
+must have been a sequence, say $u_1\cdot u_2$, with
+
+\begin{center}
+\begin{tabular}{ll}
+(b***) & $\vdash u_1 : der\;c\;r_1$\\
+       & $\vdash u_2 : r_2$\\
+\end{tabular}
+\end{center}
+
+\noindent 
+Instantiating the goal means we need to prove
+
+\[
+inj\; (r_1 \cdot r_2)\;c\;(Left(u_1\cdot u_2)) \succ_{r_1 \cdot r_2} 
+inj\; (r_1 \cdot r_2)\;c\;(Right(w_2))
+\]
+
+\noindent 
+We can simplify this according to the rules of $inj$:
+
+\[
+(inj\; r_1\;c\;u_1)\cdot u_2 \succ_{r_1 \cdot r_2} 
+(mkeps\;r_1) \cdot (inj\; r_2\;c\;w_2)
+\]
+
+\noindent
+This is what we need to prove.
+
+
 \subsubsection*{Case RL}
 
 The corresponding rule (instantiated) is: