| Contradiction of loc
| Cut of loc * 'term
| Decompose of loc * 'ident * 'ident list (* where, which principles *)
- | Discriminate of loc * 'ident
+ | Discriminate of loc * 'term
| Elim of loc * 'term * 'term option (* what to elim, which principle to use *)
| ElimType of loc * 'term
| Exact of loc * 'term