| Byinduction of loc * 'term * 'ident
| Thesisbecomes of loc * 'term
| Case of loc * string * (string * 'term) list
| ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term
| AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
| RewritingStep of
| Byinduction of loc * 'term * 'ident
| Thesisbecomes of loc * 'term
| Case of loc * string * (string * 'term) list
| ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term
| AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
| RewritingStep of