| NDestruct (_,dom,skip) -> "ndestruct ..."
| NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term what ^
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NDestruct (_,dom,skip) -> "ndestruct ..."
| NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term what ^
"...to be implemented..." ^ " " ^ "...to be implemented..."