- | Let1 of loc * 'ident * 'term * 'term
- | Bywehave of loc * 'term option * 'term * 'ident * 'term * 'ident
- | RewritingStep of loc * 'term option * 'term * 'term option
+ | ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term
+ | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term
+ | RewritingStep of
+ loc * 'term option * 'term * 'term option * Cic.name option