Nested inductive types, such as RoseTree, are fundamental in formalizing computer science, as they can model complex syntax like pattern-matching constructors. Yet, neither Rocq nor Lean currently provides adequate support for them, both positivity and generation of elimination principles being insufficient.

In this work, we introduce a new positivity condition for nested inductive type that is neither too lax nor too strict. This new positivity condition further enables us to automatically generate useful elimination principles for nested inductive types corresponding to what users expect.