§ Lean does not allow nested inductive families

• The checker is defined in terms of reduction to plain inductives, although the reduction itself is not performed before going to the kernel (it was in lean 3 but this lead to performance issues).
• The recursor for the type is basically "whatever the analogous mutual inductive would have".

inductive Const : Type _ | mk
inductive Const1 (t: Type _) : Type _ | mk : Const1 t
inductive E : Const → Type
| mk : {c : Const} → (args : Const1 (E c)) → E Const.mk
-- (kernel) invalid nested inductive datatype 'Const1',
-- nested inductive datatypes parameters cannot contain local variables.