claudio, please have a look at this

[helm.git] / helm / software / matita / tests / ng_elim.ma

diff --git a/helm/software/matita/tests/ng_elim.ma b/helm/software/matita/tests/ng_elim.ma
index b67401fde0a32273ccabdcdf6e3b19c1ab1f2834..c8998a22795d4b63a3e8e45c3f4626fe7dd7ef68 100644 (file)
--- a/helm/software/matita/tests/ng_elim.ma
+++ b/helm/software/matita/tests/ng_elim.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ng_pts.ma".
+
 ninductive nat: Type ≝
    O: nat
  | S: nat → nat.
@@ -64,10 +66,12 @@ nlet rec le_rec (n:nat) (Q: ∀D1:nat.∀D2: P D1. le n D1 D2 → Type) (p1: ?)
  ## ]
 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