-occurrence. This is a trick to make the unification algorithm ignore
-the head of the application (since the unification is essentially
-first-order) but normally operate on the arguments.
-This works for some tactics, like rewrite and replace,
-but for example not for change and other tactics that do not relay on
-unification.
+occurrence.
+
+At this point, since Coq unification algorithm is essentially
+first-order, the application of an elimination principle (of the
+form $\forall P.\forall x.(H~x)\to (P~x)$) will unify
+$x$ with \texttt{n} and $P$ with \texttt{(fun n0 : nat => m + n = n0)}.
+
+Since rewriting, replacing and several other tactics boils down to
+the application of the equality elimination principle, the previous
+trick deals the expected behaviour.