Is Agda the only implementation that supports (indexed) inductive-recursive types? Let’s forget about the extra flexibility of the recursion part allowed in Agda.