X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=a0c014251979413ea0b1edaba8e0cd26f52b47d0;hb=951069678fea0d6dcdde984320ec5057ddc57c3c;hp=d902d1380eab3b0ac781e6332c33f6603528b063;hpb=537a83ce3480e3bf4719f61f79dbed6081f5b1b2;p=helm.git

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index d902d1380..a0c014251 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1578,7 +1578,8 @@ where \texttt{H} is $\beta$-expanded over the second \texttt{n}
 occurrence. 
 
 At this point, since \COQ{} unification algorithm is essentially first-order,
-the application of an elimination principle (a term with type $\forall P.\forall
+the application of an elimination principle (a term of type\linebreak
+$\forall P.\forall
 x.(H~x)\to (P~x)$) will unify \texttt{x} with \texttt{n} and \texttt{P} with
 \texttt{(fun n0: nat => m + n = n0)}.