| Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)
| ClearBody (_,id) -> Printf.sprintf "clearbody %s" (pp_hyps [id])
| Constructor (_,n) -> "constructor " ^ string_of_int n
+ | Compose (_,t1, t2, intro_specs) ->
+ Printf.sprintf "compose %s %s%s" (term_pp t1) (term_pp t1)
+ (pp_intros_specs " as " intro_specs)
| Contradiction _ -> "contradiction"
| Cut (_, ident, term) ->
"cut " ^ term_pp term ^