Theorem statment appears reversed

pdf/grandpa.tex

@@ -359,7 +359,7 @@ We define $V_{r,v,t}$ be the set $V_{r,v}$ at time $t$ and similarly for $C_{r,v
 \begin{lemma} \label{lem:message-monotonicity-completed-estimate}
 Assume $3f < n-1$.
 Let $v,v'$ be (possibly identical) honest participants, $t,t'$ be times with $t \leq t'$, and $r$ be a round.
-Then if $V_{r,v,t} \subseteq V_{r,v',t'}$ and $C_{r,v,t} \subseteq C_{r,v',t'}$, all these sets are tolerant, and $v$ sees that $r$ is completable at time $t$, then $E_{r,v,t} \leq E_{r,v',t'}$ and $v'$ sees that $r$ is completable at time $t'$.
+Then if $V_{r,v,t} \subseteq V_{r,v',t'}$ and $C_{r,v,t} \subseteq C_{r,v',t'}$, all these sets are tolerant, and $v$ sees that $r$ is completable at time $t$, then $E_{r,v',t'} \leq E_{r,v,t}$ and $v'$ sees that $r$ is completable at time $t'$.
 \end{lemma}
 
 \begin{proof}