" with " ^ NotationPp.pp_term wwhat
| NCut (_,t) -> "ncut " ^ NotationPp.pp_term t
(*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term t
| NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term t *)
| NDestruct (_,dom,skip) -> "ndestruct ..."
| NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term what ^
" with " ^ NotationPp.pp_term wwhat
| NCut (_,t) -> "ncut " ^ NotationPp.pp_term t
(*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term t
| NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term t *)
| NDestruct (_,dom,skip) -> "ndestruct ..."
| NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term what ^