assert false ^ " " ^ assert false
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
+ | NInversion (_,what,where) -> "ninversion " ^ CicNotationPp.pp_term what ^
+ assert false ^ " " ^ assert false
| NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t
| NRewrite (_,dir,n,where) -> "nrewrite " ^
(match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^