| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false