| ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term
| AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
| RewritingStep of
| ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term
| AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
| RewritingStep of