+nqed.*)
+
+ninductive list (A:Type) : nat → Type ≝
+ nil: list A O
+ | cons: ∀n. A → list A n → list A (S n).
+
+ninductive ii: Type ≝
+ kk: list ii O → ii.
+
+nlet rec ii_rect (Q_: (∀(x_16: ii).Type)) H_kknil H_kkcons x_16 on x_16: (Q_ x_16) ≝
+ (match x_16 with
+ [ kk x_17 ⇒ list_rect ii (λx_17.Q_ (kk x_17)) H_kknil (λw.H_kkcons w (ii_rect Q_ H_kknil H_kkcons w)) x_17 ]).
\ No newline at end of file