Strongly normalizing type theory beyond induction-recursion
Yes. System F is probably the simplest example. As far as I know, you can’t prove normalisation for it in a dependent type theory with induction-recursion — you need at least impredicative prop to do so.