| Cut of loc * 'ident option * 'term
| Decompose of loc * 'ident option list
| Demodulate of loc
- | Destruct of loc * 'term
+ | Destruct of loc * 'term list option
| Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern *
'ident intros_spec
| ElimType of loc * 'term * 'term option * 'ident intros_spec
| Right of loc
| Ring of loc
| Split of loc
- | Subst of loc
| Symmetry of loc
| Transitivity of loc * 'term
(* Costruttori Aggiunti *)