+ninductive I2 : I1 → Type[0] ≝
+| k2 : ∀x.I2 x.
+
+ninductive I3 : ∀x:I1.I2 x → Type[0] ≝
+| k3 : ∀x,y.I3 x y.
+
+ninductive I4 : ∀x,y.I3 x y → Type[0] ≝
+| k4 : ∀x,y.∀z:I3 x y.I4 x y z.
+
+(*alias id "eq" = "cic:/matita/ng/logic/equality/eq.ind(1,0,2)".
+alias id "refl" = "cic:/matita/ng/logic/equality/eq.con(0,1,2)".*)
+
+ninductive II : Type[0] ≝
+| kII1 : ∀x,y,z.∀w:I4 x y z.II
+| kII2 : ∀x,y,z.∀w:I4 x y z.II.