X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fng_elim.ma;h=c8998a22795d4b63a3e8e45c3f4626fe7dd7ef68;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=b67401fde0a32273ccabdcdf6e3b19c1ab1f2834;hpb=45cf52fb31fdefdb17377aa14902d2a1ff1b11d2;p=helm.git

diff --git a/helm/software/matita/tests/ng_elim.ma b/helm/software/matita/tests/ng_elim.ma
index b67401fde..c8998a227 100644
--- 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