-from the idea behind patterns, but really fails in help using
-complex notation, since it relays on the way the user sees the
-sequent. Notation can swap arguments, or place them upside-down or
-even put them inside a bidimensional matrix. In these cases using the
-mouse to select the wanted term is probably the only way to tell the
-system exactly what you want to do.
+from the idea behind patterns, but really fails in extending to
+complex notation, since it relays on a mono-dimensional sequent representation.
+Real math notation places arguments upside-down (like in indexed sums or
+integrations) or even puts them inside a bidimensional matrix.
+In these cases using the mouse to select the wanted term is probably the
+only way to tell the system exactly what you want to do.