§ Nested vs mutual inductive types:

inductive m1
| mk: m2 -> m1

inductive m2
| mk: m1 -> m2

inductive n1: Type :=
| mk: n2 n1 -> n1

inductive n2 (a: Type): Type :=
| nil: n2 a
| cons: a -> n2 a -> n2 a