-grammar entry, acts on $H$ that has type (without notation)
-$(eq~nat~(m+n)~n)$ and discharges the head of the application and the
-first two arguments with a $?$ and selects the last argument with
-$\%$. The syntax may seem uncomfortable, but the user can simply
-select with the mouse the right part of the equivalence and left to the
-system the burden of writing down in the script file the corresponding
-pattern with $?$ and $\%$ in the right place (expecially where implicit
-arguments are hidden by the notation, like the type $nat$ in this
-example).
+grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
+and discharges the head of the application and the first two arguments with a
+$?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
+but the user can simply select with the mouse the right part of the equivalence
+and left to the system the burden of writing down in the script file the
+corresponding pattern with $?$ and $\%$ in the right place (that is not
+trivial, expecially where implicit arguments are hidden by the notation, like
+the type $nat$ in this example).