line breaking

[helm.git] / helm / papers / matita / matita2.tex

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index d902d1380eab3b0ac781e6332c33f6603528b063..a0c014251979413ea0b1edaba8e0cd26f52b47d0 100644 (file)
--- 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)}.