(match using with None -> "" | Some term -> " using " ^ term_pp term)
^ pp_intros_specs (num, idents)
| ElimType (_, term, using, num, idents) ->
(match using with None -> "" | Some term -> " using " ^ term_pp term)
^ pp_intros_specs (num, idents)
| ElimType (_, term, using, num, idents) ->