From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 30 Jan 2015 13:49:49 +0000 (+0000)
Subject: porting of basic_1 for the ng_kernel: first step ...
X-Git-Tag: make_still_working~756
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e51d01099c08e9945ea093da6fcac353db7ca23c;p=helm.git

porting of basic_1 for the ng_kernel: first step ...
---

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 9b90b9997..cdd4f35b6 100644
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -40,9 +40,6 @@ XPACKAGES := ground_2 basic_2
 LDWS := $(shell find -name "*.ldw.xml")
 TBLS := $(shell find -name "*.tbl")
 
-all:
-	../../matitac.opt
-
 # MAS ########################################################################
 
 define MAS_TEMPLATE
@@ -60,6 +57,10 @@ endef
 
 $(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG))))
 
+all:
+	@echo "  MATITAC $(PACKAGES)"
+	$(H)../../matitac.opt $(MAS)
+
 # XMAS #######################################################################
 
 define XMAS_TEMPLATE
diff --git a/matita/matita/contribs/lambdadelta/basic_1/preamble.ma b/matita/matita/contribs/lambdadelta/basic_1/preamble.ma
index c9d6a172a..2354bcc2b 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/preamble.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/preamble.ma
@@ -12,4 +12,4 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Ground-1/theory.ma".
+include "ground_1/theory.ma".
diff --git a/matita/matita/contribs/lambdadelta/ground_1/blt/defs.ma b/matita/matita/contribs/lambdadelta/ground_1/blt/defs.ma
index 009627a3b..f1eee61f5 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/blt/defs.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/blt/defs.ma
@@ -14,12 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/preamble.ma".
+include "ground_1/preamble.ma".
 
-definition blt:
- nat \to (nat \to bool)
-\def
- let rec blt (m: nat) (n: nat) on n: bool \def (match n with [O \Rightarrow 
+let rec blt (m: nat) (n: nat) on n: bool \def match n with [O \Rightarrow 
 false | (S n0) \Rightarrow (match m with [O \Rightarrow true | (S m0) 
-\Rightarrow (blt m0 n0)])]) in blt.
+\Rightarrow (blt m0 n0)])].
 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/blt/props.ma b/matita/matita/contribs/lambdadelta/ground_1/blt/props.ma
index e5b569925..689d6b45e 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/blt/props.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/blt/props.ma
@@ -14,32 +14,27 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/blt/defs.ma".
+include "ground_1/blt/defs.ma".
 
 theorem lt_blt:
  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true)))
 \def
  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to 
 (eq bool (blt y n) true)))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0 
-\def (match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat 
-n O) \to (eq bool (blt y O) true)))) with [le_n \Rightarrow (\lambda (H0: (eq 
-nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e in 
-nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) 
-\Rightarrow True])) I O H0) in (False_ind (eq bool (blt y O) true) H1))) | 
-(le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind 
-nat (S m) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) 
-with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind 
-((le (S y) m) \to (eq bool (blt y O) true)) H2)) H0))]) in (H0 (refl_equal 
-nat O))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to 
-(eq bool (blt y n) true))))).(\lambda (y: nat).(nat_ind (\lambda (n0: 
-nat).((lt n0 (S n)) \to (eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S 
-n))).(refl_equal bool true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) 
-\to (eq bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m 
-n)]) true)))).(\lambda (H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1))))) 
+\def (match H in le with [le_n \Rightarrow (\lambda (H0: (eq nat (S y) 
+O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e in nat with [O 
+\Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq bool 
+(blt y O) true) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) 
+O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e in nat with [O 
+\Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S 
+y) m) \to (eq bool (blt y O) true)) H2)) H0))]) in (H0 (refl_equal nat O))))) 
+(\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq bool (blt 
+y n) true))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n)) 
+\to (eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S n))).(refl_equal 
+bool true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) \to (eq bool 
+(match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) 
+true)))).(\lambda (H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1))))) 
 y)))) x).
-(* COMMENTS
-Initial nodes: 291
-END *)
 
 theorem le_bge:
  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq bool (blt y x) false)))
@@ -49,44 +44,34 @@ theorem le_bge:
 y)).(refl_equal bool false))) (\lambda (n: nat).(\lambda (H: ((\forall (y: 
 nat).((le n y) \to (eq bool (blt y n) false))))).(\lambda (y: nat).(nat_ind 
 (\lambda (n0: nat).((le (S n) n0) \to (eq bool (blt n0 (S n)) false))) 
-(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 in le return (\lambda (n0: 
-nat).(\lambda (_: (le ? n0)).((eq nat n0 O) \to (eq bool (blt O (S n)) 
-false)))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def 
-(eq_ind nat (S n) (\lambda (e: nat).(match e in nat return (\lambda (_: 
-nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in 
-(False_ind (eq bool (blt O (S n)) false) H2))) | (le_S m H1) \Rightarrow 
-(\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: 
-nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False 
+(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 in le with [le_n 
+\Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def (eq_ind nat (S n) 
+(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _) 
+\Rightarrow True])) I O H1) in (False_ind (eq bool (blt O (S n)) false) H2))) 
+| (le_S m H1) \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def 
+(eq_ind nat (S m) (\lambda (e: nat).(match e in nat with [O \Rightarrow False 
 | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to (eq bool 
 (blt O (S n)) false)) H3)) H1))]) in (H1 (refl_equal nat O)))) (\lambda (n0: 
 nat).(\lambda (_: (((le (S n) n0) \to (eq bool (blt n0 (S n)) 
 false)))).(\lambda (H1: (le (S n) (S n0))).(H n0 (le_S_n n n0 H1))))) y)))) 
 x).
-(* COMMENTS
-Initial nodes: 293
-END *)
 
 theorem blt_lt:
  \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) true) \to (lt y x)))
 \def
  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt 
 y n) true) \to (lt y n)))) (\lambda (y: nat).(\lambda (H: (eq bool (blt y O) 
-true)).(let H0 \def (match H in eq return (\lambda (b: bool).(\lambda (_: (eq 
-? ? b)).((eq bool b true) \to (lt y O)))) with [refl_equal \Rightarrow 
-(\lambda (H0: (eq bool (blt y O) true)).(let H1 \def (eq_ind bool (blt y O) 
-(\lambda (e: bool).(match e in bool return (\lambda (_: bool).Prop) with 
-[true \Rightarrow False | false \Rightarrow True])) I true H0) in (False_ind 
-(lt y O) H1)))]) in (H0 (refl_equal bool true))))) (\lambda (n: nat).(\lambda 
-(H: ((\forall (y: nat).((eq bool (blt y n) true) \to (lt y n))))).(\lambda 
-(y: nat).(nat_ind (\lambda (n0: nat).((eq bool (blt n0 (S n)) true) \to (lt 
-n0 (S n)))) (\lambda (_: (eq bool true true)).(le_S_n (S O) (S n) (le_n_S (S 
-O) (S n) (le_n_S O n (le_O_n n))))) (\lambda (n0: nat).(\lambda (_: (((eq 
-bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true) 
-\to (lt n0 (S n))))).(\lambda (H1: (eq bool (blt n0 n) true)).(lt_n_S n0 n (H 
-n0 H1))))) y)))) x).
-(* COMMENTS
-Initial nodes: 252
-END *)
+true)).(let H0 \def (match H in eq with [refl_equal \Rightarrow (\lambda (H0: 
+(eq bool (blt y O) true)).(let H1 \def (eq_ind bool (blt y O) (\lambda (e: 
+bool).(match e in bool with [true \Rightarrow False | false \Rightarrow 
+True])) I true H0) in (False_ind (lt y O) H1)))]) in (H0 (refl_equal bool 
+true))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq bool (blt y 
+n) true) \to (lt y n))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((eq 
+bool (blt n0 (S n)) true) \to (lt n0 (S n)))) (\lambda (_: (eq bool true 
+true)).(le_S_n (S O) (S n) (le_n_S (S O) (S n) (le_n_S O n (le_O_n n))))) 
+(\lambda (n0: nat).(\lambda (_: (((eq bool (match n0 with [O \Rightarrow true 
+| (S m) \Rightarrow (blt m n)]) true) \to (lt n0 (S n))))).(\lambda (H1: (eq 
+bool (blt n0 n) true)).(lt_n_S n0 n (H n0 H1))))) y)))) x).
 
 theorem bge_le:
  \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y)))
@@ -96,17 +81,12 @@ y n) false) \to (le n y)))) (\lambda (y: nat).(\lambda (_: (eq bool (blt y O)
 false)).(le_O_n y))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq 
 bool (blt y n) false) \to (le n y))))).(\lambda (y: nat).(nat_ind (\lambda 
 (n0: nat).((eq bool (blt n0 (S n)) false) \to (le (S n) n0))) (\lambda (H0: 
-(eq bool (blt O (S n)) false)).(let H1 \def (match H0 in eq return (\lambda 
-(b: bool).(\lambda (_: (eq ? ? b)).((eq bool b false) \to (le (S n) O)))) 
-with [refl_equal \Rightarrow (\lambda (H1: (eq bool (blt O (S n)) 
-false)).(let H2 \def (eq_ind bool (blt O (S n)) (\lambda (e: bool).(match e 
-in bool return (\lambda (_: bool).Prop) with [true \Rightarrow True | false 
-\Rightarrow False])) I false H1) in (False_ind (le (S n) O) H2)))]) in (H1 
-(refl_equal bool false)))) (\lambda (n0: nat).(\lambda (_: (((eq bool (blt n0 
-(S n)) false) \to (le (S n) n0)))).(\lambda (H1: (eq bool (blt (S n0) (S n)) 
-false)).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S n n0 (H n0 
-H1))))))) y)))) x).
-(* COMMENTS
-Initial nodes: 262
-END *)
+(eq bool (blt O (S n)) false)).(let H1 \def (match H0 in eq with [refl_equal 
+\Rightarrow (\lambda (H1: (eq bool (blt O (S n)) false)).(let H2 \def (eq_ind 
+bool (blt O (S n)) (\lambda (e: bool).(match e in bool with [true \Rightarrow 
+True | false \Rightarrow False])) I false H1) in (False_ind (le (S n) O) 
+H2)))]) in (H1 (refl_equal bool false)))) (\lambda (n0: nat).(\lambda (_: 
+(((eq bool (blt n0 (S n)) false) \to (le (S n) n0)))).(\lambda (H1: (eq bool 
+(blt (S n0) (S n)) false)).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S 
+n n0 (H n0 H1))))))) y)))) x).
 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/definitions.ma b/matita/matita/contribs/lambdadelta/ground_1/definitions.ma
index df31468aa..81a1e38f2 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/definitions.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/definitions.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/types/defs.ma".
+include "ground_1/types/defs.ma".
 
-include "Ground-1/blt/defs.ma".
+include "ground_1/blt/defs.ma".
 
-include "Ground-1/plist/defs.ma".
+include "ground_1/plist/defs.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/ext/arith.ma b/matita/matita/contribs/lambdadelta/ground_1/ext/arith.ma
index f9796e7fd..a0e72708f 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/ext/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/ext/arith.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/preamble.ma".
+include "ground_1/preamble.ma".
 
 theorem nat_dec:
  \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to 
@@ -28,36 +28,31 @@ Prop).P)) (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (eq nat O n)
 ((eq nat O n) \to (\forall (P: Prop).P)))).(or_intror (eq nat O (S n)) ((eq 
 nat O (S n)) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat O (S 
 n))).(\lambda (P: Prop).(let H1 \def (eq_ind nat O (\lambda (ee: nat).(match 
-ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) 
-\Rightarrow False])) I (S n) H0) in (False_ind P H1))))))) n2)) (\lambda (n: 
-nat).(\lambda (H: ((\forall (n2: nat).(or (eq nat n n2) ((eq nat n n2) \to 
-(\forall (P: Prop).P)))))).(\lambda (n2: nat).(nat_ind (\lambda (n0: nat).(or 
-(eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P: Prop).P)))) (or_intror 
-(eq nat (S n) O) ((eq nat (S n) O) \to (\forall (P: Prop).P)) (\lambda (H0: 
-(eq nat (S n) O)).(\lambda (P: Prop).(let H1 \def (eq_ind nat (S n) (\lambda 
-(ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow 
-False | (S _) \Rightarrow True])) I O H0) in (False_ind P H1))))) (\lambda 
-(n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall 
-(P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to (\forall (P: 
-Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to (\forall (P: 
-Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r nat n0 
-(\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P: 
-Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq nat (S n) (S 
-n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)))) (or_introl (eq nat 
-(S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P: Prop).P)) (refl_equal nat 
-(S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to (\forall (P: 
-Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to 
-(\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P: 
-Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat return 
-(\lambda (_: nat).nat) with [O \Rightarrow n | (S n3) \Rightarrow n3])) (S n) 
-(S n0) H2) in (let H4 \def (eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3) 
-\to (\forall (P0: Prop).P0))) H1 n H3) in (let H5 \def (eq_ind_r nat n0 
-(\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0: 
-Prop).P0)))) H0 n H3) in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) 
-n1).
-(* COMMENTS
-Initial nodes: 676
-END *)
+ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I (S n) H0) 
+in (False_ind P H1))))))) n2)) (\lambda (n: nat).(\lambda (H: ((\forall (n2: 
+nat).(or (eq nat n n2) ((eq nat n n2) \to (\forall (P: Prop).P)))))).(\lambda 
+(n2: nat).(nat_ind (\lambda (n0: nat).(or (eq nat (S n) n0) ((eq nat (S n) 
+n0) \to (\forall (P: Prop).P)))) (or_intror (eq nat (S n) O) ((eq nat (S n) 
+O) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat (S n) O)).(\lambda (P: 
+Prop).(let H1 \def (eq_ind nat (S n) (\lambda (ee: nat).(match ee in nat with 
+[O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind P 
+H1))))) (\lambda (n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) 
+n0) \to (\forall (P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to 
+(\forall (P: Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to 
+(\forall (P: Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r 
+nat n0 (\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to 
+(\forall (P: Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq 
+nat (S n) (S n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)))) 
+(or_introl (eq nat (S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P: 
+Prop).P)) (refl_equal nat (S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to 
+(\forall (P: Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S 
+n0)) \to (\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda 
+(P: Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat 
+with [O \Rightarrow n | (S n3) \Rightarrow n3])) (S n) (S n0) H2) in (let H4 
+\def (eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3) \to (\forall (P0: 
+Prop).P0))) H1 n H3) in (let H5 \def (eq_ind_r nat n0 (\lambda (n3: nat).(or 
+(eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0: Prop).P0)))) H0 n H3) 
+in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) n1).
 
 theorem simpl_plus_r:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n) 
@@ -66,28 +61,19 @@ theorem simpl_plus_r:
  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat 
 (plus m n) (plus p n))).(simpl_plus_l n m p (eq_ind_r nat (plus m n) (\lambda 
 (n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0: 
-nat).(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_sym n 
-p)) (plus m n) H) (plus n m) (plus_sym n m)))))).
-(* COMMENTS
-Initial nodes: 119
-END *)
+nat).(eq nat n0 (plus n p))) (plus_sym p n) (plus m n) H) (plus n m) 
+(plus_sym n m)))))).
 
 theorem minus_Sx_Sy:
  \forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
 \def
  \lambda (x: nat).(\lambda (y: nat).(refl_equal nat (minus x y))).
-(* COMMENTS
-Initial nodes: 13
-END *)
 
 theorem minus_plus_r:
  \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
 \def
  \lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0: 
 nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_sym m n))).
-(* COMMENTS
-Initial nodes: 45
-END *)
 
 theorem plus_permute_2_in_3:
  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x 
@@ -99,9 +85,6 @@ y) z) (plus (plus x z) y))))
 nat (plus (plus x z) y) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) 
 (refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_r x z 
 y)) (plus y z) (plus_sym y z)) (plus (plus x y) z) (plus_assoc_r x y z)))).
-(* COMMENTS
-Initial nodes: 163
-END *)
 
 theorem plus_permute_2_in_3_assoc:
  \forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n 
@@ -112,9 +95,6 @@ h) k) (plus n (plus k h)))))
 nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat (plus (plus n k) h) n0)) 
 (refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc_l n k 
 h)) (plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
-(* COMMENTS
-Initial nodes: 119
-END *)
 
 theorem plus_O:
  \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat 
@@ -125,27 +105,19 @@ n y) O) \to (land (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda
 (H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) 
 H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O) 
 \to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq 
-nat (plus (S n) y) O)).(let H1 \def (match H0 in eq return (\lambda (n0: 
-nat).(\lambda (_: (eq ? ? n0)).((eq nat n0 O) \to (land (eq nat (S n) O) (eq 
-nat y O))))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n) 
-y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e in 
-nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) 
-\Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y 
-O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
-(* COMMENTS
-Initial nodes: 233
-END *)
+nat (plus (S n) y) O)).(let H1 \def (match H0 in eq with [refl_equal 
+\Rightarrow (\lambda (H1: (eq nat (plus (S n) y) O)).(let H2 \def (eq_ind nat 
+(plus (S n) y) (\lambda (e: nat).(match e in nat with [O \Rightarrow False | 
+(S _) \Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq 
+nat y O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
 
 theorem minus_Sx_SO:
  \forall (x: nat).(eq nat (minus (S x) (S O)) x)
 \def
  \lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal 
 nat x) (minus x O) (minus_n_O x)).
-(* COMMENTS
-Initial nodes: 33
-END *)
 
-theorem eq_nat_dec:
+theorem nat_dec_neg:
  \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
 \def
  \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq 
@@ -163,9 +135,6 @@ nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda
 n) (S n0)) (not_eq_S n n0 H1))) (\lambda (H1: (eq nat n n0)).(or_intror (not 
 (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) (H 
 n0)))) j)))) i).
-(* COMMENTS
-Initial nodes: 401
-END *)
 
 theorem neq_eq_e:
  \forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j)) 
@@ -173,10 +142,7 @@ theorem neq_eq_e:
 \def
  \lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not 
 (eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def 
-(eq_nat_dec i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
-(* COMMENTS
-Initial nodes: 61
-END *)
+(nat_dec_neg i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
 
 theorem le_false:
  \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S 
@@ -185,42 +151,33 @@ n) m) \to P))))
  \lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P: 
 Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P: 
 Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match 
-H0 in le return (\lambda (n0: nat).(\lambda (_: (le ? n0)).((eq nat n0 O) \to 
-P))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def 
-(eq_ind nat (S n) (\lambda (e: nat).(match e in nat return (\lambda (_: 
-nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in 
-(False_ind P H2))) | (le_S m0 H1) \Rightarrow (\lambda (H2: (eq nat (S m0) 
-O)).((let H3 \def (eq_ind nat (S m0) (\lambda (e: nat).(match e in nat return 
-(\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) 
-I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))]) in (H1 (refl_equal 
-nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(\forall (P: 
-Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda (n0: nat).(nat_ind 
-(\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) 
-\to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_: (le (S 
-O) (S n))).(let H2 \def (match H0 in le return (\lambda (n1: nat).(\lambda 
-(_: (le ? n1)).((eq nat n1 O) \to P))) with [le_n \Rightarrow (\lambda (H2: 
-(eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) (\lambda (e: nat).(match e 
-in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) 
+H0 in le with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def 
+(eq_ind nat (S n) (\lambda (e: nat).(match e in nat with [O \Rightarrow False 
+| (S _) \Rightarrow True])) I O H1) in (False_ind P H2))) | (le_S m0 H1) 
+\Rightarrow (\lambda (H2: (eq nat (S m0) O)).((let H3 \def (eq_ind nat (S m0) 
+(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _) 
+\Rightarrow True])) I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))]) 
+in (H1 (refl_equal nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: 
+nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda 
+(n0: nat).(nat_ind (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to 
+((le (S n1) (S n)) \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) 
+O)).(\lambda (_: (le (S O) (S n))).(let H2 \def (match H0 in le with [le_n 
+\Rightarrow (\lambda (H2: (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) 
+(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _) 
 \Rightarrow True])) I O H2) in (False_ind P H3))) | (le_S m0 H2) \Rightarrow 
 (\lambda (H3: (eq nat (S m0) O)).((let H4 \def (eq_ind nat (S m0) (\lambda 
-(e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow 
-False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S n) m0) \to P) 
-H4)) H2))]) in (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_: 
-((\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda 
-(P: Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S 
+(e: nat).(match e in nat with [O \Rightarrow False | (S _) \Rightarrow 
+True])) I O H3) in (False_ind ((le (S n) m0) \to P) H4)) H2))]) in (H2 
+(refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P: 
+Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda (P: 
+Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S 
 n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m).
-(* COMMENTS
-Initial nodes: 409
-END *)
 
 theorem le_Sx_x:
  \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
 \def
  \lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def 
 le_Sn_n in (False_ind P (H0 x H))))).
-(* COMMENTS
-Initial nodes: 23
-END *)
 
 theorem le_n_pred:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (le (pred n) (pred m))))
@@ -229,22 +186,16 @@ theorem le_n_pred:
 (n0: nat).(le (pred n) (pred n0))) (le_n (pred n)) (\lambda (m0: 
 nat).(\lambda (_: (le n m0)).(\lambda (H1: (le (pred n) (pred m0))).(le_trans 
 (pred n) (pred m0) m0 H1 (le_pred_n m0))))) m H))).
-(* COMMENTS
-Initial nodes: 71
-END *)
 
 theorem minus_le:
  \forall (x: nat).(\forall (y: nat).(le (minus x y) x))
 \def
  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n 
-y) n))) (\lambda (_: nat).(le_n O)) (\lambda (n: nat).(\lambda (H: ((\forall 
-(y: nat).(le (minus n y) n)))).(\lambda (y: nat).(nat_ind (\lambda (n0: 
-nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0: nat).(\lambda 
-(_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow (minus n l)]) 
-(S n))).(le_S (minus n n0) n (H n0)))) y)))) x).
-(* COMMENTS
-Initial nodes: 101
-END *)
+y) n))) (\lambda (_: nat).(le_O_n O)) (\lambda (n: nat).(\lambda (H: 
+((\forall (y: nat).(le (minus n y) n)))).(\lambda (y: nat).(nat_ind (\lambda 
+(n0: nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0: 
+nat).(\lambda (_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow 
+(minus n l)]) (S n))).(le_S (minus n n0) n (H n0)))) y)))) x).
 
 theorem le_plus_minus_sym:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) 
@@ -253,9 +204,6 @@ n))))
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(eq_ind_r nat 
 (plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H) 
 (plus (minus m n) n) (plus_sym (minus m n) n)))).
-(* COMMENTS
-Initial nodes: 61
-END *)
 
 theorem le_minus_minus:
  \forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z) 
@@ -266,9 +214,6 @@ nat).(\lambda (H0: (le y z)).(simpl_le_plus_l x (minus y x) (minus z x)
 (eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat 
 z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z 
 (le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
-(* COMMENTS
-Initial nodes: 117
-END *)
 
 theorem le_minus_plus:
  \forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat 
@@ -276,10 +221,8 @@ theorem le_minus_plus:
 \def
  \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to 
 (\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y)))))) 
-(\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H in le return 
-(\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x) \to (\forall (y: 
-nat).(eq nat (minus (plus x y) O) (plus (minus x O) y)))))) with [le_n 
-\Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n: 
+(\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H in le with 
+[le_n \Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n: 
 nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y)))) 
 (\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O) 
 (minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq 
@@ -291,23 +234,18 @@ nat).((le z0 x) \to (\forall (y: nat).(eq nat (minus (plus x y) z0) (plus
 (minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S 
 z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n 
 (S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def 
-(match H0 in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) 
-\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))))) with 
-[le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2 \def (eq_ind nat 
-(S z0) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with 
-[O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq 
-nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1) 
+(match H0 in le with [le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let 
+H2 \def (eq_ind nat (S z0) (\lambda (e: nat).(match e in nat with [O 
+\Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq nat 
+(minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1) 
 \Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) 
-(\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O 
-\Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S 
-z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3)) 
-H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S 
-z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n 
-(S z0)) y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n 
-(le_S_n z0 n H1) y))))) x)))) z).
-(* COMMENTS
-Initial nodes: 603
-END *)
+(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _) 
+\Rightarrow True])) I O H2) in (False_ind ((le (S z0) m) \to (eq nat (minus 
+(plus O y) (S z0)) (plus (minus O (S z0)) y))) H3)) H1))]) in (H1 (refl_equal 
+nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S z0) n) \to (\forall (y: 
+nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) 
+y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n (le_S_n z0 n 
+H1) y))))) x)))) z).
 
 theorem le_minus:
  \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to 
@@ -317,9 +255,6 @@ theorem le_minus:
 x y) z)).(eq_ind nat (minus (plus x y) y) (\lambda (n: nat).(le n (minus z 
 y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x (minus_plus_r x 
 y))))).
-(* COMMENTS
-Initial nodes: 69
-END *)
 
 theorem le_trans_plus_r:
  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to 
@@ -327,30 +262,22 @@ theorem le_trans_plus_r:
 \def
  \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(\lambda (H: (le (plus 
 x y) z)).(le_trans y (plus x y) z (le_plus_r x y) H)))).
-(* COMMENTS
-Initial nodes: 35
-END *)
 
 theorem lt_x_O:
  \forall (x: nat).((lt x O) \to (\forall (P: Prop).P))
 \def
  \lambda (x: nat).(\lambda (H: (le (S x) O)).(\lambda (P: Prop).(let H_y \def 
 (le_n_O_eq (S x) H) in (let H0 \def (eq_ind nat O (\lambda (ee: nat).(match 
-ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) 
-\Rightarrow False])) I (S x) H_y) in (False_ind P H0))))).
-(* COMMENTS
-Initial nodes: 48
-END *)
+ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I (S x) H_y) 
+in (False_ind P H0))))).
 
 theorem le_gen_S:
  \forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n: 
 nat).(eq nat x (S n))) (\lambda (n: nat).(le m n)))))
 \def
  \lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def 
-(match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x) 
-\to (ex2 nat (\lambda (n0: nat).(eq nat x (S n0))) (\lambda (n0: nat).(le m 
-n0)))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat 
-(S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) 
+(match H in le with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind 
+nat (S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) 
 (\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S 
 m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x 
 H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat 
@@ -359,9 +286,6 @@ nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m)
 m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n: 
 nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) 
 x H1 H0))]) in (H0 (refl_equal nat x))))).
-(* COMMENTS
-Initial nodes: 261
-END *)
 
 theorem lt_x_plus_x_Sy:
  \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
@@ -369,9 +293,6 @@ theorem lt_x_plus_x_Sy:
  \lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n: 
 nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x)) 
 (le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_sym x (S y)))).
-(* COMMENTS
-Initial nodes: 83
-END *)
 
 theorem simpl_lt_plus_r:
  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m 
@@ -382,9 +303,6 @@ n p) (plus m p))).(simpl_lt_plus_l n m p (let H0 \def (eq_ind nat (plus n p)
 (\lambda (n0: nat).(lt n0 (plus m p))) H (plus p n) (plus_sym n p)) in (let 
 H1 \def (eq_ind nat (plus m p) (\lambda (n0: nat).(lt (plus p n) n0)) H0 
 (plus p m) (plus_sym m p)) in H1)))))).
-(* COMMENTS
-Initial nodes: 101
-END *)
 
 theorem minus_x_Sy:
  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S 
@@ -392,27 +310,22 @@ theorem minus_x_Sy:
 \def
  \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to 
 (eq nat (minus n y) (S (minus n (S y))))))) (\lambda (y: nat).(\lambda (H: 
-(lt y O)).(let H0 \def (match H in le return (\lambda (n: nat).(\lambda (_: 
-(le ? n)).((eq nat n O) \to (eq nat (minus O y) (S (minus O (S y))))))) with 
-[le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1 \def (eq_ind nat (S 
-y) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O 
-\Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq nat 
-(minus O y) (S (minus O (S y)))) H1))) | (le_S m H0) \Rightarrow (\lambda 
-(H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: 
-nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False 
-| (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq nat 
-(minus O y) (S (minus O (S y))))) H2)) H0))]) in (H0 (refl_equal nat O))))) 
-(\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq nat 
-(minus n y) (S (minus n (S y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0: 
-nat).((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) 
-(\lambda (_: (lt O (S n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S 
-n0))) (refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0: 
+(lt y O)).(let H0 \def (match H in le with [le_n \Rightarrow (\lambda (H0: 
+(eq nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e 
+in nat with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) in 
+(False_ind (eq nat (minus O y) (S (minus O (S y)))) H1))) | (le_S m H0) 
+\Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) 
+(\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _) 
+\Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq nat (minus O 
+y) (S (minus O (S y))))) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda 
+(n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq nat (minus n y) (S 
+(minus n (S y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 
+(S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) (\lambda (_: 
+(lt O (S n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S n0))) 
+(refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0: 
 nat).(\lambda (_: (((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S 
 n) (S n0))))))).(\lambda (H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0) 
 n H1) in (H n0 H2))))) y)))) x).
-(* COMMENTS
-Initial nodes: 383
-END *)
 
 theorem lt_plus_minus:
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus 
@@ -420,9 +333,6 @@ y (S x)))))))
 \def
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_plus_minus (S 
 x) y H))).
-(* COMMENTS
-Initial nodes: 19
-END *)
 
 theorem lt_plus_minus_r:
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y 
@@ -431,9 +341,6 @@ theorem lt_plus_minus_r:
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(eq_ind_r nat 
 (plus x (minus y (S x))) (\lambda (n: nat).(eq nat y (S n))) (lt_plus_minus x 
 y H) (plus (minus y (S x)) x) (plus_sym (minus y (S x)) x)))).
-(* COMMENTS
-Initial nodes: 69
-END *)
 
 theorem minus_x_SO:
  \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
@@ -441,29 +348,21 @@ theorem minus_x_SO:
  \lambda (x: nat).(\lambda (H: (lt O x)).(eq_ind nat (minus x O) (\lambda (n: 
 nat).(eq nat x n)) (eq_ind nat x (\lambda (n: nat).(eq nat x n)) (refl_equal 
 nat x) (minus x O) (minus_n_O x)) (S (minus x (S O))) (minus_x_Sy x O H))).
-(* COMMENTS
-Initial nodes: 77
-END *)
 
 theorem le_x_pred_y:
  \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
 \def
  \lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to 
 (le x (pred n))))) (\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def 
-(match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) 
-\to (le x O)))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let 
-H1 \def (eq_ind nat (S x) (\lambda (e: nat).(match e in nat return (\lambda 
-(_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) 
-in (False_ind (le x O) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat 
-(S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e in nat 
-return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow 
-True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) H0))]) in (H0 
-(refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt 
-x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S 
-n))).(le_S_n x n H0))))) y).
-(* COMMENTS
-Initial nodes: 189
-END *)
+(match H in le with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let H1 
+\def (eq_ind nat (S x) (\lambda (e: nat).(match e in nat with [O \Rightarrow 
+False | (S _) \Rightarrow True])) I O H0) in (False_ind (le x O) H1))) | 
+(le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind 
+nat (S m) (\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S _) 
+\Rightarrow True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) 
+H0))]) in (H0 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall 
+(x: nat).((lt x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: 
+(lt x (S n))).(le_S_n x n H0))))) y).
 
 theorem lt_le_minus:
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
@@ -471,9 +370,6 @@ theorem lt_le_minus:
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_minus x y (S 
 O) (eq_ind_r nat (plus (S O) x) (\lambda (n: nat).(le n y)) H (plus x (S O)) 
 (plus_sym x (S O)))))).
-(* COMMENTS
-Initial nodes: 57
-END *)
 
 theorem lt_le_e:
  \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P)) 
@@ -482,9 +378,6 @@ theorem lt_le_e:
  \lambda (n: nat).(\lambda (d: nat).(\lambda (P: Prop).(\lambda (H: (((lt n 
 d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in 
 (or_ind (le d n) (lt n d) P H0 H H1)))))).
-(* COMMENTS
-Initial nodes: 49
-END *)
 
 theorem lt_eq_e:
  \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) 
@@ -493,9 +386,6 @@ theorem lt_eq_e:
  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x 
 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x 
 y)).(or_ind (lt x y) (eq nat x y) P H H0 (le_lt_or_eq x y H1))))))).
-(* COMMENTS
-Initial nodes: 59
-END *)
 
 theorem lt_eq_gt_e:
  \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) 
@@ -505,9 +395,6 @@ theorem lt_eq_gt_e:
 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (((lt y x) 
 \to P))).(lt_le_e x y P H (\lambda (H2: (le y x)).(lt_eq_e y x P H1 (\lambda 
 (H3: (eq nat y x)).(H0 (sym_eq nat y x H3))) H2)))))))).
-(* COMMENTS
-Initial nodes: 79
-END *)
 
 theorem lt_gen_xS:
  \forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2 
@@ -524,9 +411,6 @@ nat).(\lambda (H0: (lt (S n) (S n0))).(or_intror (eq nat (S n) O) (ex2 nat
 (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt m n0))) 
 (ex_intro2 nat (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt 
 m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x).
-(* COMMENTS
-Initial nodes: 243
-END *)
 
 theorem le_lt_false:
  \forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P: 
@@ -534,9 +418,6 @@ Prop).P))))
 \def
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (H0: (lt 
 y x)).(\lambda (P: Prop).(False_ind P (le_not_lt x y H H0)))))).
-(* COMMENTS
-Initial nodes: 31
-END *)
 
 theorem lt_neq:
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y))))
@@ -544,9 +425,6 @@ theorem lt_neq:
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq 
 nat x y)).(let H1 \def (eq_ind nat x (\lambda (n: nat).(lt n y)) H y H0) in 
 (lt_n_n y H1))))).
-(* COMMENTS
-Initial nodes: 43
-END *)
 
 theorem arith0:
  \forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n) 
@@ -562,9 +440,6 @@ h2) (\lambda (n0: nat).(le n0 (minus (plus n h1) h2))) (le_minus_minus h2
 (le_plus_plus (plus d2 h2) n h1 h1 H (le_n h1)))) (plus h2 d2) (plus_sym h2 
 d2)) (plus h2 (plus d2 h1)) (plus_assoc_l h2 d2 h1))) (plus d2 h1) 
 (minus_plus h2 (plus d2 h1))))))).
-(* COMMENTS
-Initial nodes: 235
-END *)
 
 theorem O_minus:
  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
@@ -578,15 +453,11 @@ x0) | (S l) \Rightarrow (minus x0 l)]) O))) (\lambda (H0: (le (S x0)
 O)).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le x0 
 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H1: (eq nat O (S 
 x1))).(\lambda (_: (le x0 x1)).(let H3 \def (eq_ind nat O (\lambda (ee: 
-nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True 
-| (S _) \Rightarrow False])) I (S x1) H1) in (False_ind (eq nat (S x0) O) 
-H3))))) (le_gen_S x0 O H0))) (\lambda (n: nat).(\lambda (_: (((le (S x0) n) 
-\to (eq nat (match n with [O \Rightarrow (S x0) | (S l) \Rightarrow (minus x0 
-l)]) O)))).(\lambda (H1: (le (S x0) (S n))).(H n (le_S_n x0 n H1))))) y)))) 
-x).
-(* COMMENTS
-Initial nodes: 252
-END *)
+nat).(match ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I 
+(S x1) H1) in (False_ind (eq nat (S x0) O) H3))))) (le_gen_S x0 O H0))) 
+(\lambda (n: nat).(\lambda (_: (((le (S x0) n) \to (eq nat (match n with [O 
+\Rightarrow (S x0) | (S l) \Rightarrow (minus x0 l)]) O)))).(\lambda (H1: (le 
+(S x0) (S n))).(H n (le_S_n x0 n H1))))) y)))) x).
 
 theorem minus_minus:
  \forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y) 
@@ -608,29 +479,25 @@ y)))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le
 z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le 
 z0 n)) (eq nat O y) (\lambda (x0: nat).(\lambda (H2: (eq nat O (S 
 x0))).(\lambda (_: (le z0 x0)).(let H4 \def (eq_ind nat O (\lambda (ee: 
-nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True 
-| (S _) \Rightarrow False])) I (S x0) H2) in (False_ind (eq nat O y) H4))))) 
-(le_gen_S z0 O H)))))) (\lambda (x0: nat).(\lambda (_: ((\forall (y: 
-nat).((le (S z0) x0) \to ((le (S z0) y) \to ((eq nat (minus x0 (S z0)) (minus 
-y (S z0))) \to (eq nat x0 y))))))).(\lambda (y: nat).(nat_ind (\lambda (n: 
-nat).((le (S z0) (S x0)) \to ((le (S z0) n) \to ((eq nat (minus (S x0) (S 
-z0)) (minus n (S z0))) \to (eq nat (S x0) n))))) (\lambda (H: (le (S z0) (S 
-x0))).(\lambda (H0: (le (S z0) O)).(\lambda (_: (eq nat (minus (S x0) (S z0)) 
-(minus O (S z0)))).(let H_y \def (le_S_n z0 x0 H) in (ex2_ind nat (\lambda 
-(n: nat).(eq nat O (S n))) (\lambda (n: nat).(le z0 n)) (eq nat (S x0) O) 
-(\lambda (x1: nat).(\lambda (H2: (eq nat O (S x1))).(\lambda (_: (le z0 
-x1)).(let H4 \def (eq_ind nat O (\lambda (ee: nat).(match ee in nat return 
-(\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False])) 
-I (S x1) H2) in (False_ind (eq nat (S x0) O) H4))))) (le_gen_S z0 O H0)))))) 
-(\lambda (y0: nat).(\lambda (_: (((le (S z0) (S x0)) \to ((le (S z0) y0) \to 
-((eq nat (minus (S x0) (S z0)) (minus y0 (S z0))) \to (eq nat (S x0) 
-y0)))))).(\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) (S 
-y0))).(\lambda (H1: (eq nat (minus (S x0) (S z0)) (minus (S y0) (S 
+nat).(match ee in nat with [O \Rightarrow True | (S _) \Rightarrow False])) I 
+(S x0) H2) in (False_ind (eq nat O y) H4))))) (le_gen_S z0 O H)))))) (\lambda 
+(x0: nat).(\lambda (_: ((\forall (y: nat).((le (S z0) x0) \to ((le (S z0) y) 
+\to ((eq nat (minus x0 (S z0)) (minus y (S z0))) \to (eq nat x0 
+y))))))).(\lambda (y: nat).(nat_ind (\lambda (n: nat).((le (S z0) (S x0)) \to 
+((le (S z0) n) \to ((eq nat (minus (S x0) (S z0)) (minus n (S z0))) \to (eq 
+nat (S x0) n))))) (\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) 
+O)).(\lambda (_: (eq nat (minus (S x0) (S z0)) (minus O (S z0)))).(let H_y 
+\def (le_S_n z0 x0 H) in (ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) 
+(\lambda (n: nat).(le z0 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda 
+(H2: (eq nat O (S x1))).(\lambda (_: (le z0 x1)).(let H4 \def (eq_ind nat O 
+(\lambda (ee: nat).(match ee in nat with [O \Rightarrow True | (S _) 
+\Rightarrow False])) I (S x1) H2) in (False_ind (eq nat (S x0) O) H4))))) 
+(le_gen_S z0 O H0)))))) (\lambda (y0: nat).(\lambda (_: (((le (S z0) (S x0)) 
+\to ((le (S z0) y0) \to ((eq nat (minus (S x0) (S z0)) (minus y0 (S z0))) \to 
+(eq nat (S x0) y0)))))).(\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S 
+z0) (S y0))).(\lambda (H1: (eq nat (minus (S x0) (S z0)) (minus (S y0) (S 
 z0)))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0) 
 H1))))))) y)))) x)))) z).
-(* COMMENTS
-Initial nodes: 751
-END *)
 
 theorem plus_plus:
  \forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1: 
@@ -706,9 +573,6 @@ z0))).(\lambda (H0: (le (S x4) (S z0))).(\lambda (H1: (eq nat (plus (minus z0
 x2) y1) (plus (minus z0 x4) y2))).(f_equal nat nat S (plus x2 y2) (plus x4 
 y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3)))) 
 x1)))) z).
-(* COMMENTS
-Initial nodes: 1495
-END *)
 
 theorem le_S_minus:
  \forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to 
@@ -719,9 +583,6 @@ d h) n)).(let H0 \def (le_trans d (plus d h) n (le_plus_l d h) H) in (let H1
 \def (eq_ind nat n (\lambda (n0: nat).(le d n0)) H0 (plus (minus n h) h) 
 (le_plus_minus_sym h n (le_trans h (plus d h) n (le_plus_r d h) H))) in (le_S 
 d (minus n h) (le_minus d n h H))))))).
-(* COMMENTS
-Initial nodes: 107
-END *)
 
 theorem lt_x_pred_y:
  \forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))
@@ -729,9 +590,5 @@ theorem lt_x_pred_y:
  \lambda (x: nat).(\lambda (y: nat).(nat_ind (\lambda (n: nat).((lt x (pred 
 n)) \to (lt (S x) n))) (\lambda (H: (lt x O)).(lt_x_O x H (lt (S x) O))) 
 (\lambda (n: nat).(\lambda (_: (((lt x (pred n)) \to (lt (S x) n)))).(\lambda 
-(H0: (lt x n)).(le_S_n (S (S x)) (S n) (le_n_S (S (S x)) (S n) (le_n_S (S x) 
-n H0)))))) y)).
-(* COMMENTS
-Initial nodes: 103
-END *)
+(H0: (lt x n)).(lt_n_S x n H0)))) y)).
 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/ext/tactics.ma b/matita/matita/contribs/lambdadelta/ground_1/ext/tactics.ma
index 766db9f1f..e6e1faf02 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/ext/tactics.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/ext/tactics.ma
@@ -14,37 +14,28 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/preamble.ma".
+include "ground_1/preamble.ma".
 
 theorem insert_eq:
- \forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G: 
-((S \to Prop))).(((\forall (y: S).((P y) \to ((eq S y x) \to (G y))))) \to 
-((P x) \to (G x))))))
+ \forall (S: Type[0]).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall 
+(G: ((S \to Prop))).(((\forall (y: S).((P y) \to ((eq S y x) \to (G y))))) 
+\to ((P x) \to (G x))))))
 \def
- \lambda (S: Set).(\lambda (x: S).(\lambda (P: ((S \to Prop))).(\lambda (G: 
-((S \to Prop))).(\lambda (H: ((\forall (y: S).((P y) \to ((eq S y x) \to (G 
-y)))))).(\lambda (H0: (P x)).(H x H0 (refl_equal S x))))))).
-(* COMMENTS
-Initial nodes: 45
-END *)
+ \lambda (S: Type[0]).(\lambda (x: S).(\lambda (P: ((S \to Prop))).(\lambda 
+(G: ((S \to Prop))).(\lambda (H: ((\forall (y: S).((P y) \to ((eq S y x) \to 
+(G y)))))).(\lambda (H0: (P x)).(H x H0 (refl_equal S x))))))).
 
 theorem unintro:
- \forall (A: Set).(\forall (a: A).(\forall (P: ((A \to Prop))).(((\forall (x: 
-A).(P x))) \to (P a))))
+ \forall (A: Type[0]).(\forall (a: A).(\forall (P: ((A \to Prop))).(((\forall 
+(x: A).(P x))) \to (P a))))
 \def
- \lambda (A: Set).(\lambda (a: A).(\lambda (P: ((A \to Prop))).(\lambda (H: 
-((\forall (x: A).(P x)))).(H a)))).
-(* COMMENTS
-Initial nodes: 17
-END *)
+ \lambda (A: Type[0]).(\lambda (a: A).(\lambda (P: ((A \to Prop))).(\lambda 
+(H: ((\forall (x: A).(P x)))).(H a)))).
 
 theorem xinduction:
- \forall (A: Set).(\forall (t: A).(\forall (P: ((A \to Prop))).(((\forall (x: 
-A).((eq A t x) \to (P x)))) \to (P t))))
+ \forall (A: Type[0]).(\forall (t: A).(\forall (P: ((A \to Prop))).(((\forall 
+(x: A).((eq A t x) \to (P x)))) \to (P t))))
 \def
- \lambda (A: Set).(\lambda (t: A).(\lambda (P: ((A \to Prop))).(\lambda (H: 
-((\forall (x: A).((eq A t x) \to (P x))))).(H t (refl_equal A t))))).
-(* COMMENTS
-Initial nodes: 31
-END *)
+ \lambda (A: Type[0]).(\lambda (t: A).(\lambda (P: ((A \to Prop))).(\lambda 
+(H: ((\forall (x: A).((eq A t x) \to (P x))))).(H t (refl_equal A t))))).
 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/plist/defs.ma b/matita/matita/contribs/lambdadelta/ground_1/plist/defs.ma
index 8f9c1d3cc..cfb67e1ff 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/plist/defs.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/plist/defs.ma
@@ -14,30 +14,20 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/preamble.ma".
+include "ground_1/preamble.ma".
 
-inductive PList: Set \def
+inductive PList: Type[0] \def
 | PNil: PList
 | PCons: nat \to (nat \to (PList \to PList)).
 
-definition PConsTail:
- PList \to (nat \to (nat \to PList))
-\def
- let rec PConsTail (hds: PList) on hds: (nat \to (nat \to PList)) \def 
-(\lambda (h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow 
-(PCons h0 d0 PNil) | (PCons h d hds0) \Rightarrow (PCons h d (PConsTail hds0 
-h0 d0))]))) in PConsTail.
+let rec PConsTail (hds: PList) on hds: nat \to (nat \to PList) \def \lambda 
+(h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow (PCons h0 d0 
+PNil) | (PCons h d hds0) \Rightarrow (PCons h d (PConsTail hds0 h0 d0))])).
 
-definition Ss:
- PList \to PList
-\def
- let rec Ss (hds: PList) on hds: PList \def (match hds with [PNil \Rightarrow 
-PNil | (PCons h d hds0) \Rightarrow (PCons h (S d) (Ss hds0))]) in Ss.
+let rec Ss (hds: PList) on hds: PList \def match hds with [PNil \Rightarrow 
+PNil | (PCons h d hds0) \Rightarrow (PCons h (S d) (Ss hds0))].
 
-definition papp:
- PList \to (PList \to PList)
-\def
- let rec papp (a: PList) on a: (PList \to PList) \def (\lambda (b: 
-PList).(match a with [PNil \Rightarrow b | (PCons h d a0) \Rightarrow (PCons 
-h d (papp a0 b))])) in papp.
+let rec papp (a: PList) on a: PList \to PList \def \lambda (b: PList).(match 
+a with [PNil \Rightarrow b | (PCons h d a0) \Rightarrow (PCons h d (papp a0 
+b))]).
 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/plist/props.ma b/matita/matita/contribs/lambdadelta/ground_1/plist/props.ma
index 990397229..ce17a3c12 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/plist/props.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/plist/props.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/plist/defs.ma".
+include "ground_1/plist/defs.ma".
 
 theorem papp_ss:
  \forall (is1: PList).(\forall (is2: PList).(eq PList (papp (Ss is1) (Ss 
@@ -28,7 +28,4 @@ nat).(\lambda (p: PList).(\lambda (H: ((\forall (is2: PList).(eq PList (papp
 (Ss (papp p is2)) (\lambda (p0: PList).(eq PList (PCons n (S n0) p0) (PCons n 
 (S n0) (Ss (papp p is2))))) (refl_equal PList (PCons n (S n0) (Ss (papp p 
 is2)))) (papp (Ss p) (Ss is2)) (H is2))))))) is1).
-(* COMMENTS
-Initial nodes: 151
-END *)
 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/preamble.ma b/matita/matita/contribs/lambdadelta/ground_1/preamble.ma
index 16ff2dc44..b19f25444 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/preamble.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/preamble.ma
@@ -12,4 +12,4 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Legacy-1/theory.ma".
+include "legacy_1/theory.ma".
diff --git a/matita/matita/contribs/lambdadelta/ground_1/spare.ma b/matita/matita/contribs/lambdadelta/ground_1/spare.ma
index a966c2ae2..e3cba9bbc 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/spare.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/spare.ma
@@ -14,5 +14,5 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/theory.ma".
+include "ground_1/theory.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/theory.ma b/matita/matita/contribs/lambdadelta/ground_1/theory.ma
index 3b59dc6e8..e563c691a 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/theory.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/theory.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/ext/tactics.ma".
+include "ground_1/ext/tactics.ma".
 
-include "Ground-1/ext/arith.ma".
+include "ground_1/types/props.ma".
 
-include "Ground-1/types/props.ma".
+include "ground_1/ext/arith.ma".
 
-include "Ground-1/blt/props.ma".
+include "ground_1/blt/props.ma".
 
-include "Ground-1/plist/props.ma".
+include "ground_1/plist/props.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/types/defs.ma b/matita/matita/contribs/lambdadelta/ground_1/types/defs.ma
index f94969d88..3a7dadb64 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/types/defs.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/types/defs.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/preamble.ma".
+include "ground_1/preamble.ma".
 
 inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
 | and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))).
@@ -46,122 +46,124 @@ inductive or5 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop) (P4: Prop): Prop
 | or5_intro3: P3 \to (or5 P0 P1 P2 P3 P4)
 | or5_intro4: P4 \to (or5 P0 P1 P2 P3 P4).
 
-inductive ex3 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to 
+inductive ex3 (A0: Type[0]) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to 
 Prop): Prop \def
 | ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0 
 P0 P1 P2)))).
 
-inductive ex4 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to Prop) 
-(P3: A0 \to Prop): Prop \def
+inductive ex4 (A0: Type[0]) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to 
+Prop) (P3: A0 \to Prop): Prop \def
 | ex4_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to ((P3 x0) 
 \to (ex4 A0 P0 P1 P2 P3))))).
 
-inductive ex_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)): Prop \def
+inductive ex_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)): Prop 
+\def
 | ex_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to (ex_2 A0 A1 
 P0))).
 
-inductive ex2_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to 
-(A1 \to Prop)): Prop \def
+inductive ex2_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)) (P1: 
+A0 \to (A1 \to Prop)): Prop \def
 | ex2_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) 
 \to (ex2_2 A0 A1 P0 P1)))).
 
-inductive ex3_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to 
-(A1 \to Prop)) (P2: A0 \to (A1 \to Prop)): Prop \def
+inductive ex3_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)) (P1: 
+A0 \to (A1 \to Prop)) (P2: A0 \to (A1 \to Prop)): Prop \def
 | ex3_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) 
 \to ((P2 x0 x1) \to (ex3_2 A0 A1 P0 P1 P2))))).
 
-inductive ex4_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to 
-(A1 \to Prop)) (P2: A0 \to (A1 \to Prop)) (P3: A0 \to (A1 \to Prop)): Prop 
-\def
+inductive ex4_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)) (P1: 
+A0 \to (A1 \to Prop)) (P2: A0 \to (A1 \to Prop)) (P3: A0 \to (A1 \to Prop)): 
+Prop \def
 | ex4_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) 
 \to ((P2 x0 x1) \to ((P3 x0 x1) \to (ex4_2 A0 A1 P0 P1 P2 P3)))))).
 
-inductive ex_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
-Prop))): Prop \def
+inductive ex_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to 
+(A2 \to Prop))): Prop \def
 | ex_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 
 x2) \to (ex_3 A0 A1 A2 P0)))).
 
-inductive ex2_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
-Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))): Prop \def
+inductive ex2_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to 
+(A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))): Prop \def
 | ex2_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 
 x1 x2) \to ((P1 x0 x1 x2) \to (ex2_3 A0 A1 A2 P0 P1))))).
 
-inductive ex3_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
-Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to 
-Prop))): Prop \def
+inductive ex3_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to 
+(A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 
+\to Prop))): Prop \def
 | ex3_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 
 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to (ex3_3 A0 A1 A2 P0 P1 
 P2)))))).
 
-inductive ex4_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
-Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to 
-Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def
+inductive ex4_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to 
+(A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 
+\to Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def
 | ex4_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 
 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0 
 A1 A2 P0 P1 P2 P3))))))).
 
-inductive ex5_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
-Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to 
-Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))) (P4: A0 \to (A1 \to (A2 \to 
+inductive ex5_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to 
+(A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 
+\to Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))) (P4: A0 \to (A1 \to (A2 \to 
 Prop))): Prop \def
 | ex5_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 
 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to ((P4 x0 
 x1 x2) \to (ex5_3 A0 A1 A2 P0 P1 P2 P3 P4)))))))).
 
-inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to 
-(A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0 
-\to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
+inductive ex3_4 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (P0: 
+A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to 
+Prop)))) (P2: A0 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
 | ex3_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to 
 (ex3_4 A0 A1 A2 A3 P0 P1 P2))))))).
 
-inductive ex4_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to 
-(A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0 
-\to (A1 \to (A2 \to (A3 \to Prop)))) (P3: A0 \to (A1 \to (A2 \to (A3 \to 
-Prop)))): Prop \def
+inductive ex4_4 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (P0: 
+A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to 
+Prop)))) (P2: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P3: A0 \to (A1 \to (A2 
+\to (A3 \to Prop)))): Prop \def
 | ex4_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to 
 ((P3 x0 x1 x2 x3) \to (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)))))))).
 
-inductive ex4_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to 
-(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to 
-(A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3: 
-A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
+inductive ex4_5 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4: 
+Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to 
+(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to 
+(A4 \to Prop))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop 
+\def
 | ex4_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to 
 ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to (ex4_5 A0 A1 A2 A3 A4 P0 P1 
 P2 P3))))))))).
 
-inductive ex5_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to 
-(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to 
-(A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3: 
-A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4: A0 \to (A1 \to (A2 \to 
-(A3 \to (A4 \to Prop))))): Prop \def
+inductive ex5_5 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4: 
+Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to 
+(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to 
+(A4 \to Prop))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4: 
+A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
 | ex5_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to 
 ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 x2 x3 x4) \to 
 (ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4)))))))))).
 
-inductive ex6_6 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set) 
-(P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P1: A0 \to 
-(A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P2: A0 \to (A1 \to (A2 
-\to (A3 \to (A4 \to (A5 \to Prop)))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to 
-(A4 \to (A5 \to Prop)))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 
-\to Prop)))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to 
-Prop)))))): Prop \def
+inductive ex6_6 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4: 
+Type[0]) (A5: Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to 
+Prop)))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) 
+(P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P3: A0 \to 
+(A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P4: A0 \to (A1 \to (A2 
+\to (A3 \to (A4 \to (A5 \to Prop)))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to 
+(A4 \to (A5 \to Prop)))))): Prop \def
 | ex6_6_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1 
 x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5) 
 \to ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to (ex6_6 A0 A1 A2 
 A3 A4 A5 P0 P1 P2 P3 P4 P5)))))))))))).
 
-inductive ex6_7 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set) 
-(A6: Set) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
+inductive ex6_7 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4: 
+Type[0]) (A5: Type[0]) (A6: Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 
+\to (A5 \to (A6 \to Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to 
+(A5 \to (A6 \to Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 
+\to (A6 \to Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to 
+(A6 \to Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 
+\to Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
 Prop))))))): Prop \def
 | ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/types/props.ma b/matita/matita/contribs/lambdadelta/ground_1/types/props.ma
index 9c326f44c..7eabcfdb5 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/types/props.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/types/props.ma
@@ -14,20 +14,17 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Ground-1/types/defs.ma".
+include "ground_1/types/defs.ma".
 
 theorem ex2_sym:
- \forall (A: Set).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to 
+ \forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to 
 Prop))).((ex2 A (\lambda (x: A).(P x)) (\lambda (x: A).(Q x))) \to (ex2 A 
 (\lambda (x: A).(Q x)) (\lambda (x: A).(P x))))))
 \def
- \lambda (A: Set).(\lambda (P: ((A \to Prop))).(\lambda (Q: ((A \to 
+ \lambda (A: Type[0]).(\lambda (P: ((A \to Prop))).(\lambda (Q: ((A \to 
 Prop))).(\lambda (H: (ex2 A (\lambda (x: A).(P x)) (\lambda (x: A).(Q 
 x)))).(ex2_ind A (\lambda (x: A).(P x)) (\lambda (x: A).(Q x)) (ex2 A 
 (\lambda (x: A).(Q x)) (\lambda (x: A).(P x))) (\lambda (x: A).(\lambda (H0: 
 (P x)).(\lambda (H1: (Q x)).(ex_intro2 A (\lambda (x0: A).(Q x0)) (\lambda 
 (x0: A).(P x0)) x H1 H0)))) H)))).
-(* COMMENTS
-Initial nodes: 91
-END *)
 
diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
index 7d4696229..75e58b036 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Legacy-1/preamble.ma".
+include "legacy_1/preamble.ma".
 
-inductive eq (A: Set) (x: A): A \to Prop \def
+inductive eq (A: Type[0]) (x: A): A \to Prop \def
 | refl_equal: eq A x x.
 
 inductive True: Prop \def
@@ -29,10 +29,10 @@ inductive or (A: Prop) (B: Prop): Prop \def
 | or_introl: A \to (or A B)
 | or_intror: B \to (or A B).
 
-inductive ex (A: Set) (P: A \to Prop): Prop \def
+inductive ex (A: Type[0]) (P: A \to Prop): Prop \def
 | ex_intro: \forall (x: A).((P x) \to (ex A P)).
 
-inductive ex2 (A: Set) (P: A \to Prop) (Q: A \to Prop): Prop \def
+inductive ex2 (A: Type[0]) (P: A \to Prop) (Q: A \to Prop): Prop \def
 | ex_intro2: \forall (x: A).((P x) \to ((Q x) \to (ex2 A P Q))).
 
 definition not:
@@ -40,11 +40,11 @@ definition not:
 \def
  \lambda (A: Prop).(A \to False).
 
-inductive bool: Set \def
+inductive bool: Type[0] \def
 | true: bool
 | false: bool.
 
-inductive nat: Set \def
+inductive nat: Type[0] \def
 | O: nat
 | S: nat \to nat.
 
@@ -68,32 +68,26 @@ definition pred:
 \def
  \lambda (n: nat).(match n with [O \Rightarrow O | (S u) \Rightarrow u]).
 
-definition plus:
- nat \to (nat \to nat)
-\def
- let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n 
-with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus.
+let rec plus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with 
+[O \Rightarrow m | (S p) \Rightarrow (S (plus p m))]).
 
-definition minus:
- nat \to (nat \to nat)
-\def
- let rec minus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n 
-with [O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k) 
-| (S l) \Rightarrow (minus k l)])])) in minus.
+let rec minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with 
+[O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k) | (S 
+l) \Rightarrow (minus k l)])]).
 
-inductive Acc (A: Set) (R: A \to (A \to Prop)): A \to Prop \def
+inductive Acc (A: Type[0]) (R: A \to (A \to Prop)): A \to Prop \def
 | Acc_intro: \forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to 
 (Acc A R x)).
 
 definition well_founded:
- \forall (A: Set).(((A \to (A \to Prop))) \to Prop)
+ \forall (A: Type[0]).(((A \to (A \to Prop))) \to Prop)
 \def
- \lambda (A: Set).(\lambda (R: ((A \to (A \to Prop)))).(\forall (a: A).(Acc A 
-R a))).
+ \lambda (A: Type[0]).(\lambda (R: ((A \to (A \to Prop)))).(\forall (a: 
+A).(Acc A R a))).
 
 definition ltof:
- \forall (A: Set).(((A \to nat)) \to (A \to (A \to Prop)))
+ \forall (A: Type[0]).(((A \to nat)) \to (A \to (A \to Prop)))
 \def
- \lambda (A: Set).(\lambda (f: ((A \to nat))).(\lambda (a: A).(\lambda (b: 
-A).(lt (f a) (f b))))).
+ \lambda (A: Type[0]).(\lambda (f: ((A \to nat))).(\lambda (a: A).(\lambda 
+(b: A).(lt (f a) (f b))))).
 
diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/elim.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/elim.ma
new file mode 100644
index 000000000..75103b99a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/elim.ma
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "legacy_1/coq/defs.ma".
+
+theorem False_rect:
+ \forall (P: Type[0]).(False \to P)
+\def
+ \lambda (P: Type[0]).(\lambda (f: False).(match f in False with [])).
+
+theorem False_ind:
+ \forall (P: Prop).(False \to P)
+\def
+ \lambda (P: Prop).(False_rect P).
+
+theorem land_rect:
+ \forall (A: Prop).(\forall (B: Prop).(\forall (P: Type[0]).(((A \to (B \to 
+P))) \to ((land A B) \to P))))
+\def
+ \lambda (A: Prop).(\lambda (B: Prop).(\lambda (P: Type[0]).(\lambda (f: ((A 
+\to (B \to P)))).(\lambda (a: (land A B)).(match a in land with [(conj x x0) 
+\Rightarrow (f x x0)]))))).
+
+theorem land_ind:
+ \forall (A: Prop).(\forall (B: Prop).(\forall (P: Prop).(((A \to (B \to P))) 
+\to ((land A B) \to P))))
+\def
+ \lambda (A: Prop).(\lambda (B: Prop).(\lambda (P: Prop).(land_rect A B P))).
+
+theorem or_ind:
+ \forall (A: Prop).(\forall (B: Prop).(\forall (P: Prop).(((A \to P)) \to 
+(((B \to P)) \to ((or A B) \to P)))))
+\def
+ \lambda (A: Prop).(\lambda (B: Prop).(\lambda (P: Prop).(\lambda (f: ((A \to 
+P))).(\lambda (f0: ((B \to P))).(\lambda (o: (or A B)).(match o in or with 
+[(or_introl x) \Rightarrow (f x) | (or_intror x) \Rightarrow (f0 x)])))))).
+
+theorem ex_ind:
+ \forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (P0: 
+Prop).(((\forall (x: A).((P x) \to P0))) \to ((ex A P) \to P0))))
+\def
+ \lambda (A: Type[0]).(\lambda (P: ((A \to Prop))).(\lambda (P0: 
+Prop).(\lambda (f: ((\forall (x: A).((P x) \to P0)))).(\lambda (e: (ex A 
+P)).(match e in ex with [(ex_intro x x0) \Rightarrow (f x x0)]))))).
+
+theorem ex2_ind:
+ \forall (A: Type[0]).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to 
+Prop))).(\forall (P0: Prop).(((\forall (x: A).((P x) \to ((Q x) \to P0)))) 
+\to ((ex2 A P Q) \to P0)))))
+\def
+ \lambda (A: Type[0]).(\lambda (P: ((A \to Prop))).(\lambda (Q: ((A \to 
+Prop))).(\lambda (P0: Prop).(\lambda (f: ((\forall (x: A).((P x) \to ((Q x) 
+\to P0))))).(\lambda (e: (ex2 A P Q)).(match e in ex2 with [(ex_intro2 x x0 
+x1) \Rightarrow (f x x0 x1)])))))).
+
+theorem eq_rect:
+ \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Type[0]))).((P x) 
+\to (\forall (y: A).((eq A x y) \to (P y))))))
+\def
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to 
+Type[0]))).(\lambda (f: (P x)).(\lambda (y: A).(\lambda (e: (eq A x 
+y)).(match e in eq with [refl_equal \Rightarrow f])))))).
+
+theorem eq_ind:
+ \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to 
+(\forall (y: A).((eq A x y) \to (P y))))))
+\def
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(eq_rect A 
+x P))).
+
+let rec le_ind (n: nat) (P: (nat \to Prop)) (f: P n) (f0: (\forall (m: 
+nat).((le n m) \to ((P m) \to (P (S m)))))) (n0: nat) (l: le n n0) on l: P n0 
+\def match l in le with [le_n \Rightarrow f | (le_S m l0) \Rightarrow (f0 m 
+l0 ((le_ind n P f f0) m l0))].
+
+let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to Prop)) (f: 
+(\forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to (((\forall 
+(y: A).((R y x) \to (P y)))) \to (P x))))) (a: A) (a0: Acc A R a) on a0: P a 
+\def match a0 in Acc with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda (y: 
+A).(\lambda (r: (R y x)).((Acc_ind A R P f) y (a1 y r)))))].
+
diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma
index 0b9d97b42..f997eb49d 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma
@@ -14,98 +14,76 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Legacy-1/coq/defs.ma".
+include "legacy_1/coq/elim.ma".
 
 theorem f_equal:
- \forall (A: Set).(\forall (B: Set).(\forall (f: ((A \to B))).(\forall (x: 
-A).(\forall (y: A).((eq A x y) \to (eq B (f x) (f y)))))))
+ \forall (A: Type[0]).(\forall (B: Type[0]).(\forall (f: ((A \to 
+B))).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq B (f x) (f y)))))))
 \def
- \lambda (A: Set).(\lambda (B: Set).(\lambda (f: ((A \to B))).(\lambda (x: 
-A).(\lambda (y: A).(\lambda (H: (eq A x y)).(eq_ind A x (\lambda (a: A).(eq B 
-(f x) (f a))) (refl_equal B (f x)) y H)))))).
-(* COMMENTS
-Initial nodes: 51
-END *)
+ \lambda (A: Type[0]).(\lambda (B: Type[0]).(\lambda (f: ((A \to 
+B))).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x y)).(eq_ind A x 
+(\lambda (a: A).(eq B (f x) (f a))) (refl_equal B (f x)) y H)))))).
 
 theorem f_equal2:
- \forall (A1: Set).(\forall (A2: Set).(\forall (B: Set).(\forall (f: ((A1 \to 
-(A2 \to B)))).(\forall (x1: A1).(\forall (y1: A1).(\forall (x2: A2).(\forall 
-(y2: A2).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to (eq B (f x1 x2) (f y1 
-y2)))))))))))
-\def
- \lambda (A1: Set).(\lambda (A2: Set).(\lambda (B: Set).(\lambda (f: ((A1 \to 
-(A2 \to B)))).(\lambda (x1: A1).(\lambda (y1: A1).(\lambda (x2: A2).(\lambda 
-(y2: A2).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: A1).((eq A2 
-x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2 y2)).(eq_ind 
-A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B (f x1 x2)) y2 
-H0)) y1 H))))))))).
-(* COMMENTS
-Initial nodes: 109
-END *)
+ \forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall (B: Type[0]).(\forall 
+(f: ((A1 \to (A2 \to B)))).(\forall (x1: A1).(\forall (y1: A1).(\forall (x2: 
+A2).(\forall (y2: A2).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to (eq B (f x1 x2) 
+(f y1 y2)))))))))))
+\def
+ \lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda (B: Type[0]).(\lambda 
+(f: ((A1 \to (A2 \to B)))).(\lambda (x1: A1).(\lambda (y1: A1).(\lambda (x2: 
+A2).(\lambda (y2: A2).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: 
+A1).((eq A2 x2 y2) \to (eq B (f x1 x2) (f a y2)))) (\lambda (H0: (eq A2 x2 
+y2)).(eq_ind A2 x2 (\lambda (a: A2).(eq B (f x1 x2) (f x1 a))) (refl_equal B 
+(f x1 x2)) y2 H0)) y1 H))))))))).
 
 theorem f_equal3:
- \forall (A1: Set).(\forall (A2: Set).(\forall (A3: Set).(\forall (B: 
-Set).(\forall (f: ((A1 \to (A2 \to (A3 \to B))))).(\forall (x1: A1).(\forall 
-(y1: A1).(\forall (x2: A2).(\forall (y2: A2).(\forall (x3: A3).(\forall (y3: 
-A3).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to ((eq A3 x3 y3) \to (eq B (f x1 x2 
-x3) (f y1 y2 y3)))))))))))))))
-\def
- \lambda (A1: Set).(\lambda (A2: Set).(\lambda (A3: Set).(\lambda (B: 
-Set).(\lambda (f: ((A1 \to (A2 \to (A3 \to B))))).(\lambda (x1: A1).(\lambda 
-(y1: A1).(\lambda (x2: A2).(\lambda (y2: A2).(\lambda (x3: A3).(\lambda (y3: 
-A3).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: A1).((eq A2 x2 y2) 
-\to ((eq A3 x3 y3) \to (eq B (f x1 x2 x3) (f a y2 y3))))) (\lambda (H0: (eq 
-A2 x2 y2)).(eq_ind A2 x2 (\lambda (a: A2).((eq A3 x3 y3) \to (eq B (f x1 x2 
-x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3 x3 (\lambda (a: 
-A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2 x3)) y3 H1)) y2 
-H0)) y1 H)))))))))))).
-(* COMMENTS
-Initial nodes: 183
-END *)
+ \forall (A1: Type[0]).(\forall (A2: Type[0]).(\forall (A3: Type[0]).(\forall 
+(B: Type[0]).(\forall (f: ((A1 \to (A2 \to (A3 \to B))))).(\forall (x1: 
+A1).(\forall (y1: A1).(\forall (x2: A2).(\forall (y2: A2).(\forall (x3: 
+A3).(\forall (y3: A3).((eq A1 x1 y1) \to ((eq A2 x2 y2) \to ((eq A3 x3 y3) 
+\to (eq B (f x1 x2 x3) (f y1 y2 y3)))))))))))))))
+\def
+ \lambda (A1: Type[0]).(\lambda (A2: Type[0]).(\lambda (A3: Type[0]).(\lambda 
+(B: Type[0]).(\lambda (f: ((A1 \to (A2 \to (A3 \to B))))).(\lambda (x1: 
+A1).(\lambda (y1: A1).(\lambda (x2: A2).(\lambda (y2: A2).(\lambda (x3: 
+A3).(\lambda (y3: A3).(\lambda (H: (eq A1 x1 y1)).(eq_ind A1 x1 (\lambda (a: 
+A1).((eq A2 x2 y2) \to ((eq A3 x3 y3) \to (eq B (f x1 x2 x3) (f a y2 y3))))) 
+(\lambda (H0: (eq A2 x2 y2)).(eq_ind A2 x2 (\lambda (a: A2).((eq A3 x3 y3) 
+\to (eq B (f x1 x2 x3) (f x1 a y3)))) (\lambda (H1: (eq A3 x3 y3)).(eq_ind A3 
+x3 (\lambda (a: A3).(eq B (f x1 x2 x3) (f x1 x2 a))) (refl_equal B (f x1 x2 
+x3)) y3 H1)) y2 H0)) y1 H)))))))))))).
 
 theorem sym_eq:
- \forall (A: Set).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq A y 
+ \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).((eq A x y) \to (eq A y 
 x))))
 \def
- \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x 
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (H: (eq A x 
 y)).(eq_ind A x (\lambda (a: A).(eq A a x)) (refl_equal A x) y H)))).
-(* COMMENTS
-Initial nodes: 39
-END *)
 
 theorem eq_ind_r:
- \forall (A: Set).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to 
+ \forall (A: Type[0]).(\forall (x: A).(\forall (P: ((A \to Prop))).((P x) \to 
 (\forall (y: A).((eq A y x) \to (P y))))))
 \def
- \lambda (A: Set).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(\lambda (H: 
-(P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0) in 
-eq return (\lambda (a: A).(\lambda (_: (eq ? ? a)).(P a))) with [refl_equal 
-\Rightarrow H])))))).
-(* COMMENTS
-Initial nodes: 38
-END *)
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(\lambda 
+(H: (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0) 
+in eq with [refl_equal \Rightarrow H])))))).
 
 theorem trans_eq:
- \forall (A: Set).(\forall (x: A).(\forall (y: A).(\forall (z: A).((eq A x y) 
-\to ((eq A y z) \to (eq A x z))))))
+ \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).(\forall (z: A).((eq A 
+x y) \to ((eq A y z) \to (eq A x z))))))
 \def
- \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (z: A).(\lambda 
-(H: (eq A x y)).(\lambda (H0: (eq A y z)).(eq_ind A y (\lambda (a: A).(eq A x 
-a)) H z H0)))))).
-(* COMMENTS
-Initial nodes: 45
-END *)
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (z: 
+A).(\lambda (H: (eq A x y)).(\lambda (H0: (eq A y z)).(eq_ind A y (\lambda 
+(a: A).(eq A x a)) H z H0)))))).
 
 theorem sym_not_eq:
- \forall (A: Set).(\forall (x: A).(\forall (y: A).((not (eq A x y)) \to (not 
-(eq A y x)))))
+ \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).((not (eq A x y)) \to 
+(not (eq A y x)))))
 \def
- \lambda (A: Set).(\lambda (x: A).(\lambda (y: A).(\lambda (h1: (not (eq A x 
-y))).(\lambda (h2: (eq A y x)).(h1 (eq_ind A y (\lambda (a: A).(eq A a y)) 
-(refl_equal A y) x h2)))))).
-(* COMMENTS
-Initial nodes: 51
-END *)
+ \lambda (A: Type[0]).(\lambda (x: A).(\lambda (y: A).(\lambda (h1: (not (eq 
+A x y))).(\lambda (h2: (eq A y x)).(h1 (eq_ind A y (\lambda (a: A).(eq A a 
+y)) (refl_equal A y) x h2)))))).
 
 theorem nat_double_ind:
  \forall (R: ((nat \to (nat \to Prop)))).(((\forall (n: nat).(R O n))) \to 
@@ -120,27 +98,18 @@ nat).(nat_ind (\lambda (n0: nat).(\forall (m: nat).(R n0 m))) H (\lambda (n0:
 nat).(\lambda (H2: ((\forall (m: nat).(R n0 m)))).(\lambda (m: nat).(nat_ind 
 (\lambda (n1: nat).(R (S n0) n1)) (H0 n0) (\lambda (n1: nat).(\lambda (_: (R 
 (S n0) n1)).(H1 n0 n1 (H2 n1)))) m)))) n))))).
-(* COMMENTS
-Initial nodes: 111
-END *)
 
 theorem eq_add_S:
  \forall (n: nat).(\forall (m: nat).((eq nat (S n) (S m)) \to (eq nat n m)))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (eq nat (S n) (S 
 m))).(f_equal nat nat pred (S n) (S m) H))).
-(* COMMENTS
-Initial nodes: 33
-END *)
 
 theorem O_S:
  \forall (n: nat).(not (eq nat O (S n)))
 \def
  \lambda (n: nat).(\lambda (H: (eq nat O (S n))).(eq_ind nat (S n) (\lambda 
 (n0: nat).(IsSucc n0)) I O (sym_eq nat O (S n) H))).
-(* COMMENTS
-Initial nodes: 41
-END *)
 
 theorem not_eq_S:
  \forall (n: nat).(\forall (m: nat).((not (eq nat n m)) \to (not (eq nat (S 
@@ -148,17 +117,11 @@ n) (S m)))))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (not (eq nat n m))).(\lambda 
 (H0: (eq nat (S n) (S m))).(H (eq_add_S n m H0))))).
-(* COMMENTS
-Initial nodes: 35
-END *)
 
 theorem pred_Sn:
  \forall (m: nat).(eq nat m (pred (S m)))
 \def
  \lambda (m: nat).(refl_equal nat (pred (S m))).
-(* COMMENTS
-Initial nodes: 11
-END *)
 
 theorem S_pred:
  \forall (n: nat).(\forall (m: nat).((lt m n) \to (eq nat n (S (pred n)))))
@@ -167,9 +130,6 @@ theorem S_pred:
 (\lambda (n0: nat).(eq nat n0 (S (pred n0)))) (refl_equal nat (S (pred (S 
 m)))) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (_: (eq nat m0 
 (S (pred m0)))).(refl_equal nat (S (pred (S m0))))))) n H))).
-(* COMMENTS
-Initial nodes: 79
-END *)
 
 theorem le_trans:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((le m p) 
@@ -179,18 +139,12 @@ theorem le_trans:
 m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(le n n0)) H 
 (\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (le n m0)).(le_S n 
 m0 IHle)))) p H0))))).
-(* COMMENTS
-Initial nodes: 57
-END *)
 
 theorem le_trans_S:
  \forall (n: nat).(\forall (m: nat).((le (S n) m) \to (le n m)))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le (S n) m)).(le_trans n (S 
 n) m (le_S n n (le_n n)) H))).
-(* COMMENTS
-Initial nodes: 33
-END *)
 
 theorem le_n_S:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (le (S n) (S m))))
@@ -198,18 +152,12 @@ theorem le_n_S:
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_ind n (\lambda 
 (n0: nat).(le (S n) (S n0))) (le_n (S n)) (\lambda (m0: nat).(\lambda (_: (le 
 n m0)).(\lambda (IHle: (le (S n) (S m0))).(le_S (S n) (S m0) IHle)))) m H))).
-(* COMMENTS
-Initial nodes: 65
-END *)
 
 theorem le_O_n:
  \forall (n: nat).(le O n)
 \def
  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(le O n0)) (le_n O) (\lambda 
 (n0: nat).(\lambda (IHn: (le O n0)).(le_S O n0 IHn))) n).
-(* COMMENTS
-Initial nodes: 33
-END *)
 
 theorem le_S_n:
  \forall (n: nat).(\forall (m: nat).((le (S n) (S m)) \to (le n m)))
@@ -218,9 +166,6 @@ theorem le_S_n:
 n) (\lambda (n0: nat).(le (pred (S n)) (pred n0))) (le_n n) (\lambda (m0: 
 nat).(\lambda (H0: (le (S n) m0)).(\lambda (_: (le n (pred m0))).(le_trans_S 
 n m0 H0)))) (S m) H))).
-(* COMMENTS
-Initial nodes: 69
-END *)
 
 theorem le_Sn_O:
  \forall (n: nat).(not (le (S n) O))
@@ -228,9 +173,6 @@ theorem le_Sn_O:
  \lambda (n: nat).(\lambda (H: (le (S n) O)).(le_ind (S n) (\lambda (n0: 
 nat).(IsSucc n0)) I (\lambda (m: nat).(\lambda (_: (le (S n) m)).(\lambda (_: 
 (IsSucc m)).I))) O H)).
-(* COMMENTS
-Initial nodes: 43
-END *)
 
 theorem le_Sn_n:
  \forall (n: nat).(not (le (S n) n))
@@ -238,9 +180,6 @@ theorem le_Sn_n:
  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(not (le (S n0) n0))) (le_Sn_O 
 O) (\lambda (n0: nat).(\lambda (IHn: (not (le (S n0) n0))).(\lambda (H: (le 
 (S (S n0)) (S n0))).(IHn (le_S_n (S n0) n0 H))))) n).
-(* COMMENTS
-Initial nodes: 57
-END *)
 
 theorem le_antisym:
  \forall (n: nat).(\forall (m: nat).((le n m) \to ((le m n) \to (eq nat n 
@@ -252,17 +191,11 @@ nat n)) (\lambda (m0: nat).(\lambda (H: (le n m0)).(\lambda (_: (((le m0 n)
 \to (eq nat n m0)))).(\lambda (H1: (le (S m0) n)).(False_ind (eq nat n (S 
 m0)) (let H2 \def (le_trans (S m0) n m0 H1 H) in ((let H3 \def (le_Sn_n m0) 
 in (\lambda (H4: (le (S m0) m0)).(H3 H4))) H2))))))) m h))).
-(* COMMENTS
-Initial nodes: 119
-END *)
 
 theorem le_n_O_eq:
  \forall (n: nat).((le n O) \to (eq nat O n))
 \def
  \lambda (n: nat).(\lambda (H: (le n O)).(le_antisym O n (le_O_n n) H)).
-(* COMMENTS
-Initial nodes: 19
-END *)
 
 theorem le_elim_rel:
  \forall (P: ((nat \to (nat \to Prop)))).(((\forall (p: nat).(P O p))) \to 
@@ -279,51 +212,33 @@ m)).(le_ind (S n0) (\lambda (n1: nat).(P (S n0) n1)) (H0 n0 n0 (le_n n0) (IHn
 n0 (le_n n0))) (\lambda (m0: nat).(\lambda (H1: (le (S n0) m0)).(\lambda (_: 
 (P (S n0) m0)).(H0 n0 m0 (le_trans_S n0 m0 H1) (IHn m0 (le_trans_S n0 m0 
 H1)))))) m Le))))) n)))).
-(* COMMENTS
-Initial nodes: 181
-END *)
 
 theorem lt_n_n:
  \forall (n: nat).(not (lt n n))
 \def
  le_Sn_n.
-(* COMMENTS
-Initial nodes: 1
-END *)
 
 theorem lt_n_S:
  \forall (n: nat).(\forall (m: nat).((lt n m) \to (lt (S n) (S m))))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_n_S (S n) m 
 H))).
-(* COMMENTS
-Initial nodes: 19
-END *)
 
 theorem lt_n_Sn:
  \forall (n: nat).(lt n (S n))
 \def
  \lambda (n: nat).(le_n (S n)).
-(* COMMENTS
-Initial nodes: 7
-END *)
 
 theorem lt_S_n:
  \forall (n: nat).(\forall (m: nat).((lt (S n) (S m)) \to (lt n m)))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (S n) (S m))).(le_S_n (S 
 n) m H))).
-(* COMMENTS
-Initial nodes: 23
-END *)
 
 theorem lt_n_O:
  \forall (n: nat).(not (lt n O))
 \def
  le_Sn_O.
-(* COMMENTS
-Initial nodes: 1
-END *)
 
 theorem lt_trans:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((lt m p) 
@@ -333,25 +248,16 @@ theorem lt_trans:
 m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0)) (le_S 
 (S n) m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle: (lt 
 n m0)).(le_S (S n) m0 IHle)))) p H0))))).
-(* COMMENTS
-Initial nodes: 71
-END *)
 
 theorem lt_O_Sn:
  \forall (n: nat).(lt O (S n))
 \def
  \lambda (n: nat).(le_n_S O n (le_O_n n)).
-(* COMMENTS
-Initial nodes: 11
-END *)
 
 theorem lt_le_S:
  \forall (n: nat).(\forall (p: nat).((lt n p) \to (le (S n) p)))
 \def
  \lambda (n: nat).(\lambda (p: nat).(\lambda (H: (lt n p)).H)).
-(* COMMENTS
-Initial nodes: 11
-END *)
 
 theorem le_not_lt:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (not (lt m n))))
@@ -360,17 +266,11 @@ theorem le_not_lt:
 (n0: nat).(not (lt n0 n))) (lt_n_n n) (\lambda (m0: nat).(\lambda (_: (le n 
 m0)).(\lambda (IHle: (not (lt m0 n))).(\lambda (H1: (lt (S m0) n)).(IHle 
 (le_trans_S (S m0) n H1)))))) m H))).
-(* COMMENTS
-Initial nodes: 67
-END *)
 
 theorem le_lt_n_Sm:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (lt n (S m))))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(le_n_S n m H))).
-(* COMMENTS
-Initial nodes: 17
-END *)
 
 theorem le_lt_trans:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to ((lt m p) 
@@ -380,9 +280,6 @@ theorem le_lt_trans:
 m)).(\lambda (H0: (lt m p)).(le_ind (S m) (\lambda (n0: nat).(lt n n0)) 
 (le_n_S n m H) (\lambda (m0: nat).(\lambda (_: (le (S m) m0)).(\lambda (IHle: 
 (lt n m0)).(le_S (S n) m0 IHle)))) p H0))))).
-(* COMMENTS
-Initial nodes: 69
-END *)
 
 theorem lt_le_trans:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to ((le m p) 
@@ -392,27 +289,18 @@ theorem lt_le_trans:
 m)).(\lambda (H0: (le m p)).(le_ind m (\lambda (n0: nat).(lt n n0)) H 
 (\lambda (m0: nat).(\lambda (_: (le m m0)).(\lambda (IHle: (lt n m0)).(le_S 
 (S n) m0 IHle)))) p H0))))).
-(* COMMENTS
-Initial nodes: 59
-END *)
 
 theorem lt_le_weak:
  \forall (n: nat).(\forall (m: nat).((lt n m) \to (le n m)))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n m)).(le_trans_S n m 
 H))).
-(* COMMENTS
-Initial nodes: 17
-END *)
 
 theorem lt_n_Sm_le:
  \forall (n: nat).(\forall (m: nat).((lt n (S m)) \to (le n m)))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt n (S m))).(le_S_n n m 
 H))).
-(* COMMENTS
-Initial nodes: 19
-END *)
 
 theorem le_lt_or_eq:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (or (lt n m) (eq nat n m))))
@@ -422,9 +310,6 @@ theorem le_lt_or_eq:
 (refl_equal nat n)) (\lambda (m0: nat).(\lambda (H0: (le n m0)).(\lambda (_: 
 (or (lt n m0) (eq nat n m0))).(or_introl (lt n (S m0)) (eq nat n (S m0)) 
 (le_n_S n m0 H0))))) m H))).
-(* COMMENTS
-Initial nodes: 109
-END *)
 
 theorem le_or_lt:
  \forall (n: nat).(\forall (m: nat).(or (le n m) (lt m n)))
@@ -438,9 +323,6 @@ n0))).(or_ind (le n0 m0) (lt m0 n0) (or (le (S n0) (S m0)) (lt (S m0) (S
 n0))) (\lambda (H0: (le n0 m0)).(or_introl (le (S n0) (S m0)) (lt (S m0) (S 
 n0)) (le_n_S n0 m0 H0))) (\lambda (H0: (lt m0 n0)).(or_intror (le (S n0) (S 
 m0)) (lt (S m0) (S n0)) (le_n_S (S m0) n0 H0))) H)))) n m)).
-(* COMMENTS
-Initial nodes: 209
-END *)
 
 theorem plus_n_O:
  \forall (n: nat).(eq nat n (plus n O))
@@ -448,9 +330,6 @@ theorem plus_n_O:
  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (plus n0 O))) 
 (refl_equal nat O) (\lambda (n0: nat).(\lambda (H: (eq nat n0 (plus n0 
 O))).(f_equal nat nat S n0 (plus n0 O) H))) n).
-(* COMMENTS
-Initial nodes: 57
-END *)
 
 theorem plus_n_Sm:
  \forall (n: nat).(\forall (m: nat).(eq nat (S (plus n m)) (plus n (S m))))
@@ -459,9 +338,6 @@ theorem plus_n_Sm:
 (plus n0 n)) (plus n0 (S n)))) (refl_equal nat (S n)) (\lambda (n0: 
 nat).(\lambda (H: (eq nat (S (plus n0 n)) (plus n0 (S n)))).(f_equal nat nat 
 S (S (plus n0 n)) (plus n0 (S n)) H))) m)).
-(* COMMENTS
-Initial nodes: 85
-END *)
 
 theorem plus_sym:
  \forall (n: nat).(\forall (m: nat).(eq nat (plus n m) (plus m n)))
@@ -471,9 +347,6 @@ n0 m) (plus m n0))) (plus_n_O m) (\lambda (y: nat).(\lambda (H: (eq nat (plus
 y m) (plus m y))).(eq_ind nat (S (plus m y)) (\lambda (n0: nat).(eq nat (S 
 (plus y m)) n0)) (f_equal nat nat S (plus y m) (plus m y) H) (plus m (S y)) 
 (plus_n_Sm m y)))) n)).
-(* COMMENTS
-Initial nodes: 111
-END *)
 
 theorem plus_Snm_nSm:
  \forall (n: nat).(\forall (m: nat).(eq nat (plus (S n) m) (plus n (S m))))
@@ -482,9 +355,6 @@ theorem plus_Snm_nSm:
 nat).(eq nat (S n0) (plus n (S m)))) (eq_ind_r nat (plus (S m) n) (\lambda 
 (n0: nat).(eq nat (S (plus m n)) n0)) (refl_equal nat (plus (S m) n)) (plus n 
 (S m)) (plus_sym n (S m))) (plus n m) (plus_sym n m))).
-(* COMMENTS
-Initial nodes: 99
-END *)
 
 theorem plus_assoc_l:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus n (plus m 
@@ -495,9 +365,6 @@ nat).(eq nat (plus n0 (plus m p)) (plus (plus n0 m) p))) (refl_equal nat
 (plus m p)) (\lambda (n0: nat).(\lambda (H: (eq nat (plus n0 (plus m p)) 
 (plus (plus n0 m) p))).(f_equal nat nat S (plus n0 (plus m p)) (plus (plus n0 
 m) p) H))) n))).
-(* COMMENTS
-Initial nodes: 101
-END *)
 
 theorem plus_assoc_r:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(eq nat (plus (plus n 
@@ -505,9 +372,6 @@ m) p) (plus n (plus m p)))))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(sym_eq nat (plus n 
 (plus m p)) (plus (plus n m) p) (plus_assoc_l n m p)))).
-(* COMMENTS
-Initial nodes: 37
-END *)
 
 theorem simpl_plus_l:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus n m) 
@@ -521,9 +385,6 @@ nat).(\lambda (IHn: ((\forall (m: nat).(\forall (p: nat).((eq nat (plus n0 m)
 nat).(\lambda (H: (eq nat (S (plus n0 m)) (S (plus n0 p)))).(IHn m p (IHn 
 (plus n0 m) (plus n0 p) (f_equal nat nat (plus n0) (plus n0 m) (plus n0 p) 
 (eq_add_S (plus n0 m) (plus n0 p) H))))))))) n).
-(* COMMENTS
-Initial nodes: 161
-END *)
 
 theorem minus_n_O:
  \forall (n: nat).(eq nat n (minus n O))
@@ -531,9 +392,6 @@ theorem minus_n_O:
  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat n0 (minus n0 O))) 
 (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat n0 (minus n0 
 O))).(refl_equal nat (S n0)))) n).
-(* COMMENTS
-Initial nodes: 47
-END *)
 
 theorem minus_n_n:
  \forall (n: nat).(eq nat O (minus n n))
@@ -541,9 +399,6 @@ theorem minus_n_n:
  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat O (minus n0 n0))) 
 (refl_equal nat O) (\lambda (n0: nat).(\lambda (IHn: (eq nat O (minus n0 
 n0))).IHn)) n).
-(* COMMENTS
-Initial nodes: 41
-END *)
 
 theorem minus_Sn_m:
  \forall (n: nat).(\forall (m: nat).((le m n) \to (eq nat (S (minus n m)) 
@@ -555,9 +410,6 @@ n0)))) (\lambda (p: nat).(f_equal nat nat S (minus p O) p (sym_eq nat p
 (minus p O) (minus_n_O p)))) (\lambda (p: nat).(\lambda (q: nat).(\lambda (_: 
 (le p q)).(\lambda (H0: (eq nat (S (minus q p)) (match p with [O \Rightarrow 
 (S q) | (S l) \Rightarrow (minus q l)]))).H0)))) m n Le))).
-(* COMMENTS
-Initial nodes: 111
-END *)
 
 theorem plus_minus:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat n (plus m p)) 
@@ -573,18 +425,12 @@ p)) in (\lambda (H2: (eq nat O (S (plus n0 p)))).(H1 H2))) H0))))) (\lambda
 (n0: nat).(\lambda (m0: nat).(\lambda (H: (((eq nat m0 (plus n0 p)) \to (eq 
 nat p (minus m0 n0))))).(\lambda (H0: (eq nat (S m0) (S (plus n0 p)))).(H 
 (eq_add_S m0 (plus n0 p) H0)))))) m n))).
-(* COMMENTS
-Initial nodes: 199
-END *)
 
 theorem minus_plus:
  \forall (n: nat).(\forall (m: nat).(eq nat (minus (plus n m) n) m))
 \def
  \lambda (n: nat).(\lambda (m: nat).(sym_eq nat m (minus (plus n m) n) 
 (plus_minus (plus n m) n m (refl_equal nat (plus n m))))).
-(* COMMENTS
-Initial nodes: 41
-END *)
 
 theorem le_pred_n:
  \forall (n: nat).(le (pred n) n)
@@ -592,9 +438,6 @@ theorem le_pred_n:
  \lambda (n: nat).(nat_ind (\lambda (n0: nat).(le (pred n0) n0)) (le_n O) 
 (\lambda (n0: nat).(\lambda (_: (le (pred n0) n0)).(le_S (pred (S n0)) n0 
 (le_n n0)))) n).
-(* COMMENTS
-Initial nodes: 43
-END *)
 
 theorem le_plus_l:
  \forall (n: nat).(\forall (m: nat).(le n (plus n m)))
@@ -603,9 +446,6 @@ theorem le_plus_l:
 n0 m)))) (\lambda (m: nat).(le_O_n m)) (\lambda (n0: nat).(\lambda (IHn: 
 ((\forall (m: nat).(le n0 (plus n0 m))))).(\lambda (m: nat).(le_n_S n0 (plus 
 n0 m) (IHn m))))) n).
-(* COMMENTS
-Initial nodes: 55
-END *)
 
 theorem le_plus_r:
  \forall (n: nat).(\forall (m: nat).(le m (plus n m)))
@@ -613,9 +453,6 @@ theorem le_plus_r:
  \lambda (n: nat).(\lambda (m: nat).(nat_ind (\lambda (n0: nat).(le m (plus 
 n0 m))) (le_n m) (\lambda (n0: nat).(\lambda (H: (le m (plus n0 m))).(le_S m 
 (plus n0 m) H))) n)).
-(* COMMENTS
-Initial nodes: 47
-END *)
 
 theorem simpl_le_plus_l:
  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((le (plus p n) (plus p 
@@ -628,9 +465,6 @@ nat).(\lambda (IHp: ((\forall (n: nat).(\forall (m: nat).((le (plus p0 n)
 (plus p0 m)) \to (le n m)))))).(\lambda (n: nat).(\lambda (m: nat).(\lambda 
 (H: (le (S (plus p0 n)) (S (plus p0 m)))).(IHp n m (le_S_n (plus p0 n) (plus 
 p0 m) H))))))) p).
-(* COMMENTS
-Initial nodes: 113
-END *)
 
 theorem le_plus_trans:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le n 
@@ -638,9 +472,6 @@ theorem le_plus_trans:
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (le n 
 m)).(le_trans n m (plus m p) H (le_plus_l m p))))).
-(* COMMENTS
-Initial nodes: 31
-END *)
 
 theorem le_reg_l:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((le n m) \to (le (plus 
@@ -651,9 +482,6 @@ nat).((le n m) \to (le (plus n0 n) (plus n0 m)))) (\lambda (H: (le n m)).H)
 (\lambda (p0: nat).(\lambda (IHp: (((le n m) \to (le (plus p0 n) (plus p0 
 m))))).(\lambda (H: (le n m)).(le_n_S (plus p0 n) (plus p0 m) (IHp H))))) 
 p))).
-(* COMMENTS
-Initial nodes: 85
-END *)
 
 theorem le_plus_plus:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le 
@@ -664,9 +492,6 @@ nat).(\lambda (H: (le n m)).(\lambda (H0: (le p q)).(le_ind n (\lambda (n0:
 nat).(le (plus n p) (plus n0 q))) (le_reg_l p q n H0) (\lambda (m0: 
 nat).(\lambda (_: (le n m0)).(\lambda (H2: (le (plus n p) (plus m0 q))).(le_S 
 (plus n p) (plus m0 q) H2)))) m H)))))).
-(* COMMENTS
-Initial nodes: 91
-END *)
 
 theorem le_plus_minus:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus n (minus m 
@@ -677,9 +502,6 @@ n)))))
 (\lambda (p: nat).(minus_n_O p)) (\lambda (p: nat).(\lambda (q: nat).(\lambda 
 (_: (le p q)).(\lambda (H0: (eq nat q (plus p (minus q p)))).(f_equal nat nat 
 S q (plus p (minus q p)) H0))))) n m Le))).
-(* COMMENTS
-Initial nodes: 91
-END *)
 
 theorem le_plus_minus_r:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat (plus n (minus m 
@@ -687,9 +509,6 @@ n)) m)))
 \def
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(sym_eq nat m 
 (plus n (minus m n)) (le_plus_minus n m H)))).
-(* COMMENTS
-Initial nodes: 33
-END *)
 
 theorem simpl_lt_plus_l:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt (plus p n) (plus p 
@@ -700,9 +519,6 @@ nat).((lt (plus n0 n) (plus n0 m)) \to (lt n m))) (\lambda (H: (lt n m)).H)
 (\lambda (p0: nat).(\lambda (IHp: (((lt (plus p0 n) (plus p0 m)) \to (lt n 
 m)))).(\lambda (H: (lt (S (plus p0 n)) (S (plus p0 m)))).(IHp (le_S_n (S 
 (plus p0 n)) (plus p0 m) H))))) p))).
-(* COMMENTS
-Initial nodes: 99
-END *)
 
 theorem lt_reg_l:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus 
@@ -713,9 +529,6 @@ nat).((lt n m) \to (lt (plus n0 n) (plus n0 m)))) (\lambda (H: (lt n m)).H)
 (\lambda (p0: nat).(\lambda (IHp: (((lt n m) \to (lt (plus p0 n) (plus p0 
 m))))).(\lambda (H: (lt n m)).(lt_n_S (plus p0 n) (plus p0 m) (IHp H))))) 
 p))).
-(* COMMENTS
-Initial nodes: 85
-END *)
 
 theorem lt_reg_r:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((lt n m) \to (lt (plus 
@@ -727,9 +540,6 @@ nat (plus p m) (\lambda (n0: nat).(lt (plus p n) n0)) (nat_ind (\lambda (n0:
 nat).(lt (plus n0 n) (plus n0 m))) H (\lambda (n0: nat).(\lambda (_: (lt 
 (plus n0 n) (plus n0 m))).(lt_reg_l n m (S n0) H))) p) (plus m p) (plus_sym m 
 p)) (plus n p) (plus_sym n p))))).
-(* COMMENTS
-Initial nodes: 129
-END *)
 
 theorem le_lt_plus_plus:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((le 
@@ -739,9 +549,6 @@ n m) \to ((lt p q) \to (lt (plus n p) (plus m q)))))))
 nat).(\lambda (H: (le n m)).(\lambda (H0: (le (S p) q)).(eq_ind_r nat (plus n 
 (S p)) (\lambda (n0: nat).(le n0 (plus m q))) (le_plus_plus n m (S p) q H H0) 
 (plus (S n) p) (plus_Snm_nSm n p))))))).
-(* COMMENTS
-Initial nodes: 75
-END *)
 
 theorem lt_le_plus_plus:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt 
@@ -750,9 +557,6 @@ n m) \to ((le p q) \to (lt (plus n p) (plus m q)))))))
  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q: 
 nat).(\lambda (H: (le (S n) m)).(\lambda (H0: (le p q)).(le_plus_plus (S n) m 
 p q H H0)))))).
-(* COMMENTS
-Initial nodes: 37
-END *)
 
 theorem lt_plus_plus:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).(\forall (q: nat).((lt 
@@ -761,14 +565,11 @@ n m) \to ((lt p q) \to (lt (plus n p) (plus m q)))))))
  \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (q: 
 nat).(\lambda (H: (lt n m)).(\lambda (H0: (lt p q)).(lt_le_plus_plus n m p q 
 H (lt_le_weak p q H0))))))).
-(* COMMENTS
-Initial nodes: 39
-END *)
 
 theorem well_founded_ltof:
- \forall (A: Set).(\forall (f: ((A \to nat))).(well_founded A (ltof A f)))
+ \forall (A: Type[0]).(\forall (f: ((A \to nat))).(well_founded A (ltof A f)))
 \def
- \lambda (A: Set).(\lambda (f: ((A \to nat))).(let H \def (\lambda (n: 
+ \lambda (A: Type[0]).(\lambda (f: ((A \to nat))).(let H \def (\lambda (n: 
 nat).(nat_ind (\lambda (n0: nat).(\forall (a: A).((lt (f a) n0) \to (Acc A 
 (ltof A f) a)))) (\lambda (a: A).(\lambda (H: (lt (f a) O)).(False_ind (Acc A 
 (ltof A f) a) (let H0 \def H in ((let H1 \def (lt_n_O (f a)) in (\lambda (H2: 
@@ -778,17 +579,11 @@ nat).(nat_ind (\lambda (n0: nat).(\forall (a: A).((lt (f a) n0) \to (Acc A
 (ltfafb: (lt (f b) (f a))).(IHn b (lt_le_trans (f b) (f a) n0 ltfafb 
 (lt_n_Sm_le (f a) n0 ltSma)))))))))) n)) in (\lambda (a: A).(H (S (f a)) a 
 (le_n (S (f a))))))).
-(* COMMENTS
-Initial nodes: 189
-END *)
 
 theorem lt_wf:
  well_founded nat lt
 \def
  well_founded_ltof nat (\lambda (m: nat).m).
-(* COMMENTS
-Initial nodes: 7
-END *)
 
 theorem lt_wf_ind:
  \forall (p: nat).(\forall (P: ((nat \to Prop))).(((\forall (n: 
@@ -799,7 +594,4 @@ nat).(((\forall (m: nat).((lt m n) \to (P m)))) \to (P n))))).(Acc_ind nat lt
 (\lambda (n: nat).(P n)) (\lambda (x: nat).(\lambda (_: ((\forall (y: 
 nat).((lt y x) \to (Acc nat lt y))))).(\lambda (H1: ((\forall (y: nat).((lt y 
 x) \to (P y))))).(H x H1)))) p (lt_wf p)))).
-(* COMMENTS
-Initial nodes: 77
-END *)
 
diff --git a/matita/matita/contribs/lambdadelta/legacy_1/definitions.ma b/matita/matita/contribs/lambdadelta/legacy_1/definitions.ma
index 63fc85890..bcdc2a0a8 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/definitions.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/definitions.ma
@@ -14,5 +14,5 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Legacy-1/coq/defs.ma".
+include "legacy_1/coq/defs.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/legacy_1/preamble.ma b/matita/matita/contribs/lambdadelta/legacy_1/preamble.ma
index 96c1bc1fa..5466cb15e 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/preamble.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/preamble.ma
@@ -12,4 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basics/pts.ma".
+
 inductive False: Prop \def .
diff --git a/matita/matita/contribs/lambdadelta/legacy_1/spare.ma b/matita/matita/contribs/lambdadelta/legacy_1/spare.ma
index 77939a1b6..b276321ed 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/spare.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/spare.ma
@@ -14,5 +14,5 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Legacy-1/theory.ma".
+include "legacy_1/theory.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/legacy_1/theory.ma b/matita/matita/contribs/lambdadelta/legacy_1/theory.ma
index 4ee597e09..17a1ec960 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/theory.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/theory.ma
@@ -14,5 +14,5 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Legacy-1/coq/props.ma".
+include "legacy_1/coq/props.ma".