-%The latter is applied to all the goals opened by \texttt{split}
-%
-%(here we have two goals, the two sides of the logic and). The first
-%goal $B$ (with $A$ in the context) is proved by the first sequence of
-%tactics \texttt{rewrite} and \texttt{assumption}. Then we move to the
-%second goal with the separator ``\texttt{|}''.
-%
-%Giving serious examples here is rather difficult, since they are hard
-%to read without the interactive tool. To help the reader in
-%understanding the following considerations we just give few common
-%usage examples without a proof context.
-%
-%\begin{grafite}
-% elim z; try assumption; [ ... | ... ].
-% elim z; first [ assumption | reflexivity | id ].
-%\end{grafite}
-%
-%The first example goes by induction on a term \texttt{z} and applies
-%the tactic \texttt{assumption} to each opened goal eventually recovering if
-%\texttt{assumption} fails. Here we are asking the system to close all
-%trivial cases and then we branch on the remaining with ``\texttt{[}''.
-%The second example goes again by induction on \texttt{z} and tries to
-%close each opened goal first with \texttt{assumption}, if it fails it
-%tries \texttt{reflexivity} and finally \texttt{id}
-%that is the tactic that leaves the goal untouched without failing.
-%
-%Note that in the common implementation of tacticals both lines are
-%compositions of tacticals and in particular they are a single
-%statement (i.e. derived from the same non terminal entry of the
-%grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
-%this is not true, since each atomic tactic or punctuation is considered
-%a single statement.
-
-\subsubsection{Common issues of tactic(als)-based proof languages}
-We will examine the two main problems of tactic(als)-based proof script: