| Contradiction _ -> "contradiction"
| Cut (_, ident, term) ->
"cut " ^ term_pp term ^
(match ident with None -> "" | Some id -> " as " ^ id)
| Decompose (_, names) ->
| Contradiction _ -> "contradiction"
| Cut (_, ident, term) ->
"cut " ^ term_pp term ^
(match ident with None -> "" | Some id -> " as " ^ id)
| Decompose (_, names) ->