| Discriminate (_, term) -> "discriminate " ^ term_pp term
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ term_pp term ^
| Discriminate (_, term) -> "discriminate " ^ term_pp term
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ term_pp term ^