1) GrafiteAst.NEval => GrafiteAst.NReduce

[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..dfded53ee2ed82759aa93e1b078c40c0d9018806 100644 (file)
--- a/helm/software/matita/tests/ng_elim.ma
+++ b/helm/software/matita/tests/ng_elim.ma
@@ -64,10 +64,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