\subsubsection{Tactics supporting patterns}
+\TODO{Grazie ai pattern, rispetto a Coq noi abbiamo per esempio la possibilita' di fare riduzioni profonde!!!}
+
\TODO{mergiare con il successivo facendo notare che i patterns sono una
interfaccia comune per le tattiche}