(* *)
(**************************************************************************)
+include "ng_pts.ma".
+
ninductive nat: Type ≝
O: nat
| S: nat → nat.
## ]
nqed.*)
-include "list/list.ma".
+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 → ii.
+ 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