| Cut (_, term) -> "cut " ^ pp_term_ast term
| Decompose (_, ident, principles) ->
sprintf "decompose %s %s" (pp_idents principles) ident
| Cut (_, term) -> "cut " ^ pp_term_ast term
| Decompose (_, ident, principles) ->
sprintf "decompose %s %s" (pp_idents principles) ident
| Elim (_, term, using) ->
sprintf "elim " ^ pp_term_ast term ^
(match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
| Elim (_, term, using) ->
sprintf "elim " ^ pp_term_ast term ^
(match using with None -> "" | Some term -> " using " ^ pp_term_ast term)