Cleaning up proof part

diff --cc doc/iotcloud.tex
index a0e8abe636bdcc54d322d3ea51ad95eb0a51d6f3,af1b1bb12a19e01e0d3332063a0dcaa7e86d9323..f92126a2b96d543e7c14802003c91915648ea86f
--- 1/doc/iotcloud.tex
--- 2/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@@ -969,17 -951,12 +951,14 @@@ call them $\mathsf{t}$ and $\mathsf{u}
  Then $\mathsf{t}$ is in the path of $\mathsf{u}$. \r
  \end{lem}\r
  \begin{proof}\r
- By contradiction, we will prove that if $\mathsf{t}$ is not in the path of \r
- $\mathsf{u}$, then it is impossible for client $\mathsf{C}$ to receive both\r
- messages without throwing any errors. Clearly $\mathsf{C}$ will throw an error \r
- if $\mathsf{s_t = s_u}$. So $\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ \r
- receives $\mathsf{u}$ before $\mathsf{t}$, this will cause it to throw an \r
- error, so $\mathsf{t}$ is received before $\mathsf{u}$.\r
- \r
- Assume that $\mathsf{t}$ is not in the path of $\mathsf{u}$. Take $\mathsf{u}$ \r
- to be the packet of smallest sequence number for which this occurs, and \r
- $\mathsf{t}$ be the packet with greatest sequence number for this $\mathsf{u}$. \r
- We will prove that an error occurs upon receipt of $\mathsf{u}$.\r
 -Assume otherwise. Then there are some pairs $\mathsf{(t,u)}$ that violate this lemma. Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized and $\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$.\r
++Assume otherwise. Then there are some pairs $\mathsf{(t,u)}$ that violate this lemma. \r
++Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized and \r
++$\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$.\r
+ \r
+ Clearly $\mathsf{C}$ will throw an error if $\mathsf{s_t = s_u}$. So \r
+ $\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ receives $\mathsf{u}$ before \r
+ $\mathsf{t}$, this will cause it to throw an error, so $\mathsf{t}$ is received \r
+ before $\mathsf{u}$. We will prove that an error occurs upon receipt of $\mathsf{u}$.\r
  \r
  Let $\mathsf{r_1}$ be the earliest member of the path of $\mathsf{t}$ that is \r
  not in the path of $\mathsf{u}$, and $\mathsf{q}$ be its parent. Message \r