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)}.