inductive m1| mk: m2 -> m1inductive m2| mk: m1 -> m2inductive n1: Type :=| mk: n2 n1 -> n1inductive n2 (a: Type): Type :=| nil: n2 a| cons: a -> n2 a -> n2 ainductive m1| mk: m2 -> m1inductive m2| mk: m1 -> m2inductive n1: Type :=| mk: n2 n1 -> n1inductive n2 (a: Type): Type :=| nil: n2 a| cons: a -> n2 a -> n2 a