typos

practical.tex

@@ -4,8 +4,8 @@ not make use of type schemes and is, therefore, incomplete w.r.t. the
 system of Section~\ref{sec:static}. In particular, as we
 explained in Section~\ref{ssec:algorithm}, in the absence of type
 schemes it is not always possible to prove that $\forall v, \forall t,
-v \in t \text{~or~} v \not\in \lnot t$. Since this is property does
-not hold only for $\lambda$-expressions, then not using type schemes 
+v \in t \text{~or~} v \not\in \lnot t$. Since this property cease
+to hold only for $\lambda$-expressions, then not using type schemes 
 yields less precise typing only for tests $\ifty{e}t{e_1}{e_2}$ where $e$
 has a functional type, that is the value tested will be a $\lambda$
 abstraction This seems like a reasonable compromise between the