]> matita.cs.unibo.it Git - helm.git/commitdiff
line breaking
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 1 Feb 2006 23:12:00 +0000 (23:12 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 1 Feb 2006 23:12:00 +0000 (23:12 +0000)
helm/papers/matita/matita2.tex

index d902d1380eab3b0ac781e6332c33f6603528b063..a0c014251979413ea0b1edaba8e0cd26f52b47d0 100644 (file)
@@ -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)}.