From ab2f735d97d2b9c965f13527d5f6f61048d29b22 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 27 Apr 2016 16:25:05 +0000
Subject: [PATCH] exportation of lambdadelta 1 with flavoured let recs

---
 matita/components/content/notationPp.ml       |  5 +--
 .../contribs/lambdadelta/basic_1/A/fwd.ma     |  2 +-
 .../contribs/lambdadelta/basic_1/C/defs.ma    | 10 +++---
 .../contribs/lambdadelta/basic_1/C/fwd.ma     |  2 +-
 .../contribs/lambdadelta/basic_1/T/defs.ma    |  6 ++--
 .../contribs/lambdadelta/basic_1/T/fwd.ma     |  2 +-
 .../lambdadelta/basic_1/aplus/defs.ma         |  4 +--
 .../contribs/lambdadelta/basic_1/app/defs.ma  |  9 +++---
 .../contribs/lambdadelta/basic_1/aprem/fwd.ma |  2 +-
 .../contribs/lambdadelta/basic_1/arity/fwd.ma |  2 +-
 .../lambdadelta/basic_1/asucc/defs.ma         |  2 +-
 .../contribs/lambdadelta/basic_1/clear/fwd.ma |  2 +-
 .../contribs/lambdadelta/basic_1/clen/defs.ma |  4 +--
 .../contribs/lambdadelta/basic_1/cnt/fwd.ma   |  2 +-
 .../contribs/lambdadelta/basic_1/csuba/fwd.ma |  2 +-
 .../contribs/lambdadelta/basic_1/csubc/fwd.ma |  2 +-
 .../lambdadelta/basic_1/csubst0/fwd.ma        |  2 +-
 .../contribs/lambdadelta/basic_1/csubt/fwd.ma |  2 +-
 .../contribs/lambdadelta/basic_1/csubv/fwd.ma | 31 ++++++++++---------
 .../contribs/lambdadelta/basic_1/drop/fwd.ma  |  2 +-
 .../lambdadelta/basic_1/drop1/defs.ma         |  2 +-
 .../contribs/lambdadelta/basic_1/drop1/fwd.ma | 16 +++++-----
 .../contribs/lambdadelta/basic_1/ex0/fwd.ma   |  2 +-
 .../contribs/lambdadelta/basic_1/leq/fwd.ma   |  2 +-
 .../contribs/lambdadelta/basic_1/lift/defs.ma | 14 ++++-----
 .../lambdadelta/basic_1/lift1/defs.ma         | 18 +++++------
 .../contribs/lambdadelta/basic_1/llt/defs.ma  |  5 +--
 .../lambdadelta/basic_1/next_plus/defs.ma     |  4 +--
 .../contribs/lambdadelta/basic_1/nf2/defs.ma  |  2 +-
 .../contribs/lambdadelta/basic_1/pc3/left.ma  |  2 +-
 .../contribs/lambdadelta/basic_1/pr0/fwd.ma   |  2 +-
 .../contribs/lambdadelta/basic_1/pr1/fwd.ma   |  2 +-
 .../contribs/lambdadelta/basic_1/pr3/fwd.ma   |  2 +-
 .../contribs/lambdadelta/basic_1/sc3/defs.ma  |  2 +-
 .../contribs/lambdadelta/basic_1/sn3/defs.ma  |  2 +-
 .../contribs/lambdadelta/basic_1/sn3/fwd.ma   |  2 +-
 .../contribs/lambdadelta/basic_1/sty0/fwd.ma  |  2 +-
 .../contribs/lambdadelta/basic_1/sty1/fwd.ma  | 12 +++----
 .../lambdadelta/basic_1/subst/defs.ma         |  4 +--
 .../lambdadelta/basic_1/subst0/fwd.ma         |  2 +-
 .../lambdadelta/basic_1/tlist/defs.ma         | 14 ++++-----
 .../contribs/lambdadelta/basic_1/tlt/defs.ma  |  4 +--
 .../contribs/lambdadelta/basic_1/ty3/fwd.ma   | 18 +++++------
 .../contribs/lambdadelta/basic_1/wcpr0/fwd.ma | 14 ++++-----
 .../contribs/lambdadelta/basic_1/wf3/fwd.ma   |  2 +-
 .../contribs/lambdadelta/ground_1/blt/defs.ma |  6 ++--
 .../lambdadelta/ground_1/plist/defs.ma        | 17 +++++-----
 .../contribs/lambdadelta/legacy_1/coq/defs.ma | 10 +++---
 .../contribs/lambdadelta/legacy_1/coq/fwd.ma  |  4 +--
 49 files changed, 144 insertions(+), 139 deletions(-)

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index 49002d108..369a0fa28 100644
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -314,7 +314,7 @@ let pp_obj pp_term = function
     string_of_source source ^
     "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ 
     " \\def {" ^ pp_fields pp_term fields ^ "\n}"
- | Ast.LetRec (kind, definitions, (source, _, _)) ->
+ | Ast.LetRec (kind, definitions, (source, flavour, _)) ->
     let rec get_guard i = function
        | []                   -> assert false (* Ast.Implicit `JustOne *)
        | [term, _] when i = 1 -> term
@@ -332,9 +332,10 @@ let pp_obj pp_term = function
 	  (pp_term (get_guard i params))
 	  (pp_term typ) (pp_term body)
     in
-    sprintf "%slet %s %s"
+    sprintf "%s%s %s %s"
       (string_of_source source)
       (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
+      (NCicPp.string_of_flavour flavour)
       (String.concat " and " (List.map map definitions))
 
 let rec pp_value (status: #NCic.status) = function
diff --git a/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
index a0f6f0931..9e2eb7d8e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/A/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/A/defs.ma".
 
-implied let rec A_rect (P: (A \to Type[0])) (f: (\forall (n: nat).(\forall 
+implied rec lemma A_rect (P: (A \to Type[0])) (f: (\forall (n: nat).(\forall 
 (n0: nat).(P (ASort n n0))))) (f0: (\forall (a: A).((P a) \to (\forall (a0: 
 A).((P a0) \to (P (AHead a a0))))))) (a: A) on a: P a \def match a with 
 [(ASort n n0) \Rightarrow (f n n0) | (AHead a0 a1) \Rightarrow (f0 a0 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma
index 2f08ba725..9d41d8ce5 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/C/defs.ma
@@ -20,8 +20,8 @@ inductive C: Type[0] \def
 | CSort: nat \to C
 | CHead: C \to (K \to (T \to C)).
 
-let rec cweight (c: C) on c: nat \def match c with [(CSort _) \Rightarrow O | 
-(CHead c0 _ t) \Rightarrow (plus (cweight c0) (tweight t))].
+rec definition cweight (c: C) on c: nat \def match c with [(CSort _) 
+\Rightarrow O | (CHead c0 _ t) \Rightarrow (plus (cweight c0) (tweight t))].
 
 definition clt:
  C \to (C \to Prop)
@@ -33,7 +33,7 @@ definition cle:
 \def
  \lambda (c1: C).(\lambda (c2: C).(le (cweight c1) (cweight c2))).
 
-let rec CTail (k: K) (t: T) (c: C) on c: C \def match c with [(CSort n) 
-\Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead (CTail k 
-t d) h u)].
+rec definition CTail (k: K) (t: T) (c: C) on c: C \def match c with [(CSort 
+n) \Rightarrow (CHead (CSort n) k t) | (CHead d h u) \Rightarrow (CHead 
+(CTail k t d) h u)].
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/C/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/C/fwd.ma
index 675a0863b..43d43fc71 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/C/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/C/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/C/defs.ma".
 
-implied let rec C_rect (P: (C \to Type[0])) (f: (\forall (n: nat).(P (CSort 
+implied rec lemma C_rect (P: (C \to Type[0])) (f: (\forall (n: nat).(P (CSort 
 n)))) (f0: (\forall (c: C).((P c) \to (\forall (k: K).(\forall (t: T).(P 
 (CHead c k t))))))) (c: C) on c: P c \def match c with [(CSort n) \Rightarrow 
 (f n) | (CHead c0 k t) \Rightarrow (f0 c0 ((C_rect P f f0) c0) k t)].
diff --git a/matita/matita/contribs/lambdadelta/basic_1/T/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/T/defs.ma
index aad94671c..0eeff13ba 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/T/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/T/defs.ma
@@ -34,9 +34,9 @@ inductive T: Type[0] \def
 | TLRef: nat \to T
 | THead: K \to (T \to (T \to T)).
 
-let rec tweight (t: T) on t: nat \def match t with [(TSort _) \Rightarrow (S 
-O) | (TLRef _) \Rightarrow (S O) | (THead _ u t0) \Rightarrow (S (plus 
-(tweight u) (tweight t0)))].
+rec definition tweight (t: T) on t: nat \def match t with [(TSort _) 
+\Rightarrow (S O) | (TLRef _) \Rightarrow (S O) | (THead _ u t0) \Rightarrow 
+(S (plus (tweight u) (tweight t0)))].
 
 definition tle:
  T \to (T \to Prop)
diff --git a/matita/matita/contribs/lambdadelta/basic_1/T/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/T/fwd.ma
index 159a24468..5e1833cc1 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/T/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/T/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/T/defs.ma".
 
-implied let rec T_rect (P: (T \to Type[0])) (f: (\forall (n: nat).(P (TSort 
+implied rec lemma T_rect (P: (T \to Type[0])) (f: (\forall (n: nat).(P (TSort 
 n)))) (f0: (\forall (n: nat).(P (TLRef n)))) (f1: (\forall (k: K).(\forall 
 (t: T).((P t) \to (\forall (t0: T).((P t0) \to (P (THead k t t0)))))))) (t: 
 T) on t: P t \def match t with [(TSort n) \Rightarrow (f n) | (TLRef n) 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
index c26b3c286..f339331a6 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/aplus/defs.ma
@@ -16,6 +16,6 @@
 
 include "basic_1/asucc/defs.ma".
 
-let rec aplus (g: G) (a: A) (n: nat) on n: A \def match n with [O \Rightarrow 
-a | (S n0) \Rightarrow (asucc g (aplus g a n0))].
+rec definition aplus (g: G) (a: A) (n: nat) on n: A \def match n with [O 
+\Rightarrow a | (S n0) \Rightarrow (asucc g (aplus g a n0))].
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/app/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/app/defs.ma
index 40efddbbd..32ec12f51 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/app/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/app/defs.ma
@@ -16,9 +16,10 @@
 
 include "basic_1/C/defs.ma".
 
-let rec cbk (c: C) on c: nat \def match c with [(CSort m) \Rightarrow m | 
-(CHead c0 _ _) \Rightarrow (cbk c0)].
+rec definition cbk (c: C) on c: nat \def match c with [(CSort m) \Rightarrow 
+m | (CHead c0 _ _) \Rightarrow (cbk c0)].
 
-let rec app1 (c: C) on c: T \to T \def \lambda (t: T).(match c with [(CSort 
-_) \Rightarrow t | (CHead c0 k u) \Rightarrow (app1 c0 (THead k u t))]).
+rec definition app1 (c: C) on c: T \to T \def \lambda (t: T).(match c with 
+[(CSort _) \Rightarrow t | (CHead c0 k u) \Rightarrow (app1 c0 (THead k u 
+t))]).
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/aprem/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/aprem/fwd.ma
index 43f3bcec5..3f415a4c1 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/aprem/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/aprem/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/aprem/defs.ma".
 
-implied let rec aprem_ind (P: (nat \to (A \to (A \to Prop)))) (f: (\forall 
+implied rec lemma aprem_ind (P: (nat \to (A \to (A \to Prop)))) (f: (\forall 
 (a1: A).(\forall (a2: A).(P O (AHead a1 a2) a1)))) (f0: (\forall (a2: 
 A).(\forall (a: A).(\forall (i: nat).((aprem i a2 a) \to ((P i a2 a) \to 
 (\forall (a1: A).(P (S i) (AHead a1 a2) a)))))))) (n: nat) (a: A) (a0: A) 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/arity/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/arity/fwd.ma
index 58775a829..78211905a 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/arity/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/arity/fwd.ma
@@ -20,7 +20,7 @@ include "basic_1/leq/asucc.ma".
 
 include "basic_1/getl/drop.ma".
 
-implied let rec arity_ind (g: G) (P: (C \to (T \to (A \to Prop)))) (f: 
+implied rec lemma arity_ind (g: G) (P: (C \to (T \to (A \to Prop)))) (f: 
 (\forall (c: C).(\forall (n: nat).(P c (TSort n) (ASort O n))))) (f0: 
 (\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c 
 (CHead d (Bind Abbr) u)) \to (\forall (a: A).((arity g d u a) \to ((P d u a) 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/asucc/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/asucc/defs.ma
index 303985054..520f8e375 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/asucc/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/asucc/defs.ma
@@ -18,7 +18,7 @@ include "basic_1/A/defs.ma".
 
 include "basic_1/G/defs.ma".
 
-let rec asucc (g: G) (l: A) on l: A \def match l with [(ASort n0 n) 
+rec definition asucc (g: G) (l: A) on l: A \def match l with [(ASort n0 n) 
 \Rightarrow (match n0 with [O \Rightarrow (ASort O (next g n)) | (S h) 
 \Rightarrow (ASort h n)]) | (AHead a1 a2) \Rightarrow (AHead a1 (asucc g 
 a2))].
diff --git a/matita/matita/contribs/lambdadelta/basic_1/clear/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/clear/fwd.ma
index 478e65cca..1b05b45a8 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/clear/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/clear/fwd.ma
@@ -18,7 +18,7 @@ include "basic_1/clear/defs.ma".
 
 include "basic_1/C/fwd.ma".
 
-implied let rec clear_ind (P: (C \to (C \to Prop))) (f: (\forall (b: 
+implied rec lemma clear_ind (P: (C \to (C \to Prop))) (f: (\forall (b: 
 B).(\forall (e: C).(\forall (u: T).(P (CHead e (Bind b) u) (CHead e (Bind b) 
 u)))))) (f0: (\forall (e: C).(\forall (c: C).((clear e c) \to ((P e c) \to 
 (\forall (f0: F).(\forall (u: T).(P (CHead e (Flat f0) u) c)))))))) (c: C) 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/clen/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/clen/defs.ma
index 1230db5c8..64209a6f7 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/clen/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/clen/defs.ma
@@ -18,6 +18,6 @@ include "basic_1/C/defs.ma".
 
 include "basic_1/s/defs.ma".
 
-let rec clen (c: C) on c: nat \def match c with [(CSort _) \Rightarrow O | 
-(CHead c0 k _) \Rightarrow (s k (clen c0))].
+rec definition clen (c: C) on c: nat \def match c with [(CSort _) \Rightarrow 
+O | (CHead c0 k _) \Rightarrow (s k (clen c0))].
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/cnt/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/cnt/fwd.ma
index 1019462ab..922737699 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/cnt/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/cnt/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/cnt/defs.ma".
 
-implied let rec cnt_ind (P: (T \to Prop)) (f: (\forall (n: nat).(P (TSort 
+implied rec lemma cnt_ind (P: (T \to Prop)) (f: (\forall (n: nat).(P (TSort 
 n)))) (f0: (\forall (t: T).((cnt t) \to ((P t) \to (\forall (k: K).(\forall 
 (v: T).(P (THead k v t)))))))) (t: T) (c: cnt t) on c: P t \def match c with 
 [(cnt_sort n) \Rightarrow (f n) | (cnt_head t0 c0 k v) \Rightarrow (f0 t0 c0 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/csuba/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/csuba/fwd.ma
index 2f082fa2a..b94c9c8d4 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csuba/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csuba/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/csuba/defs.ma".
 
-implied let rec csuba_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n: 
+implied rec lemma csuba_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n: 
 nat).(P (CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csuba 
 g c1 c2) \to ((P c1 c2) \to (\forall (k: K).(\forall (u: T).(P (CHead c1 k u) 
 (CHead c2 k u))))))))) (f1: (\forall (c1: C).(\forall (c2: C).((csuba g c1 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubc/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/csubc/fwd.ma
index a63e6baac..22f68a288 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csubc/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubc/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/csubc/defs.ma".
 
-implied let rec csubc_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n: 
+implied rec lemma csubc_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n: 
 nat).(P (CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubc 
 g c1 c2) \to ((P c1 c2) \to (\forall (k: K).(\forall (v: T).(P (CHead c1 k v) 
 (CHead c2 k v))))))))) (f1: (\forall (c1: C).(\forall (c2: C).((csubc g c1 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubst0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/csubst0/fwd.ma
index 724d7c5a9..a267513d1 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csubst0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubst0/fwd.ma
@@ -18,7 +18,7 @@ include "basic_1/csubst0/defs.ma".
 
 include "basic_1/C/fwd.ma".
 
-implied let rec csubst0_ind (P: (nat \to (T \to (C \to (C \to Prop))))) (f: 
+implied rec lemma csubst0_ind (P: (nat \to (T \to (C \to (C \to Prop))))) (f: 
 (\forall (k: K).(\forall (i: nat).(\forall (v: T).(\forall (u1: T).(\forall 
 (u2: T).((subst0 i v u1 u2) \to (\forall (c: C).(P (s k i) v (CHead c k u1) 
 (CHead c k u2)))))))))) (f0: (\forall (k: K).(\forall (i: nat).(\forall (c1: 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubt/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/csubt/fwd.ma
index cd82088fe..eb571467a 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csubt/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubt/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/csubt/defs.ma".
 
-implied let rec csubt_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n: 
+implied rec lemma csubt_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (n: 
 nat).(P (CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubt 
 g c1 c2) \to ((P c1 c2) \to (\forall (k: K).(\forall (u: T).(P (CHead c1 k u) 
 (CHead c2 k u))))))))) (f1: (\forall (c1: C).(\forall (c2: C).((csubt g c1 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma
index ebc5ee513..23883b412 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/csubv/fwd.ma
@@ -16,19 +16,20 @@
 
 include "basic_1/csubv/defs.ma".
 
-implied let rec csubv_ind (P: (C \to (C \to Prop))) (f: (\forall (n: nat).(P 
-(CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubv c1 c2) 
-\to ((P c1 c2) \to (\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Bind Void) 
-v1) (CHead c2 (Bind Void) v2))))))))) (f1: (\forall (c1: C).(\forall (c2: 
-C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (b1: B).((not (eq B b1 Void)) 
-\to (\forall (b2: B).(\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Bind b1) 
-v1) (CHead c2 (Bind b2) v2)))))))))))) (f2: (\forall (c1: C).(\forall (c2: 
-C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (f2: F).(\forall (f3: 
-F).(\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Flat f2) v1) (CHead c2 
-(Flat f3) v2))))))))))) (c: C) (c0: C) (c1: csubv c c0) on c1: P c c0 \def 
-match c1 with [(csubv_sort n) \Rightarrow (f n) | (csubv_void c2 c3 c4 v1 v2) 
-\Rightarrow (f0 c2 c3 c4 ((csubv_ind P f f0 f1 f2) c2 c3 c4) v1 v2) | 
-(csubv_bind c2 c3 c4 b1 n b2 v1 v2) \Rightarrow (f1 c2 c3 c4 ((csubv_ind P f 
-f0 f1 f2) c2 c3 c4) b1 n b2 v1 v2) | (csubv_flat c2 c3 c4 f3 f4 v1 v2) 
-\Rightarrow (f2 c2 c3 c4 ((csubv_ind P f f0 f1 f2) c2 c3 c4) f3 f4 v1 v2)].
+implied rec lemma csubv_ind (P: (C \to (C \to Prop))) (f: (\forall (n: 
+nat).(P (CSort n) (CSort n)))) (f0: (\forall (c1: C).(\forall (c2: C).((csubv 
+c1 c2) \to ((P c1 c2) \to (\forall (v1: T).(\forall (v2: T).(P (CHead c1 
+(Bind Void) v1) (CHead c2 (Bind Void) v2))))))))) (f1: (\forall (c1: 
+C).(\forall (c2: C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (b1: B).((not 
+(eq B b1 Void)) \to (\forall (b2: B).(\forall (v1: T).(\forall (v2: T).(P 
+(CHead c1 (Bind b1) v1) (CHead c2 (Bind b2) v2)))))))))))) (f2: (\forall (c1: 
+C).(\forall (c2: C).((csubv c1 c2) \to ((P c1 c2) \to (\forall (f2: 
+F).(\forall (f3: F).(\forall (v1: T).(\forall (v2: T).(P (CHead c1 (Flat f2) 
+v1) (CHead c2 (Flat f3) v2))))))))))) (c: C) (c0: C) (c1: csubv c c0) on c1: 
+P c c0 \def match c1 with [(csubv_sort n) \Rightarrow (f n) | (csubv_void c2 
+c3 c4 v1 v2) \Rightarrow (f0 c2 c3 c4 ((csubv_ind P f f0 f1 f2) c2 c3 c4) v1 
+v2) | (csubv_bind c2 c3 c4 b1 n b2 v1 v2) \Rightarrow (f1 c2 c3 c4 
+((csubv_ind P f f0 f1 f2) c2 c3 c4) b1 n b2 v1 v2) | (csubv_flat c2 c3 c4 f3 
+f4 v1 v2) \Rightarrow (f2 c2 c3 c4 ((csubv_ind P f f0 f1 f2) c2 c3 c4) f3 f4 
+v1 v2)].
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/drop/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/drop/fwd.ma
index a77911cae..0b7876eea 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/drop/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/drop/fwd.ma
@@ -22,7 +22,7 @@ include "basic_1/r/props.ma".
 
 include "basic_1/C/fwd.ma".
 
-implied let rec drop_ind (P: (nat \to (nat \to (C \to (C \to Prop))))) (f: 
+implied rec lemma drop_ind (P: (nat \to (nat \to (C \to (C \to Prop))))) (f: 
 (\forall (c: C).(P O O c c))) (f0: (\forall (k: K).(\forall (h: nat).(\forall 
 (c: C).(\forall (e: C).((drop (r k h) O c e) \to ((P (r k h) O c e) \to 
 (\forall (u: T).(P (S h) O (CHead c k u) e))))))))) (f1: (\forall (k: 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/drop1/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/drop1/defs.ma
index ff42adbf5..41b084879 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/drop1/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/drop1/defs.ma
@@ -24,7 +24,7 @@ inductive drop1: PList \to (C \to (C \to Prop)) \def
 nat).((drop h d c1 c2) \to (\forall (c3: C).(\forall (hds: PList).((drop1 hds 
 c2 c3) \to (drop1 (PCons h d hds) c1 c3)))))))).
 
-let rec ptrans (hds: PList) on hds: nat \to PList \def \lambda (i: 
+rec definition ptrans (hds: PList) on hds: nat \to PList \def \lambda (i: 
 nat).(match hds with [PNil \Rightarrow PNil | (PCons h d hds0) \Rightarrow 
 (let j \def (trans hds0 i) in (let q \def (ptrans hds0 i) in (match (blt j d) 
 with [true \Rightarrow (PCons h (minus d (S j)) q) | false \Rightarrow 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/drop1/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/drop1/fwd.ma
index 3270fe008..319591895 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/drop1/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/drop1/fwd.ma
@@ -16,14 +16,14 @@
 
 include "basic_1/drop1/defs.ma".
 
-implied let rec drop1_ind (P: (PList \to (C \to (C \to Prop)))) (f: (\forall 
-(c: C).(P PNil c c))) (f0: (\forall (c1: C).(\forall (c2: C).(\forall (h: 
-nat).(\forall (d: nat).((drop h d c1 c2) \to (\forall (c3: C).(\forall (hds: 
-PList).((drop1 hds c2 c3) \to ((P hds c2 c3) \to (P (PCons h d hds) c1 
-c3))))))))))) (p: PList) (c: C) (c0: C) (d: drop1 p c c0) on d: P p c c0 \def 
-match d with [(drop1_nil c1) \Rightarrow (f c1) | (drop1_cons c1 c2 h d0 d1 
-c3 hds d2) \Rightarrow (f0 c1 c2 h d0 d1 c3 hds d2 ((drop1_ind P f f0) hds c2 
-c3 d2))].
+implied rec lemma drop1_ind (P: (PList \to (C \to (C \to Prop)))) (f: 
+(\forall (c: C).(P PNil c c))) (f0: (\forall (c1: C).(\forall (c2: 
+C).(\forall (h: nat).(\forall (d: nat).((drop h d c1 c2) \to (\forall (c3: 
+C).(\forall (hds: PList).((drop1 hds c2 c3) \to ((P hds c2 c3) \to (P (PCons 
+h d hds) c1 c3))))))))))) (p: PList) (c: C) (c0: C) (d: drop1 p c c0) on d: P 
+p c c0 \def match d with [(drop1_nil c1) \Rightarrow (f c1) | (drop1_cons c1 
+c2 h d0 d1 c3 hds d2) \Rightarrow (f0 c1 c2 h d0 d1 c3 hds d2 ((drop1_ind P f 
+f0) hds c2 c3 d2))].
 
 lemma drop1_gen_pnil:
  \forall (c1: C).(\forall (c2: C).((drop1 PNil c1 c2) \to (eq C c1 c2)))
diff --git a/matita/matita/contribs/lambdadelta/basic_1/ex0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/ex0/fwd.ma
index 31e071b63..248d07e06 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/ex0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ex0/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/ex0/defs.ma".
 
-implied let rec leqz_ind (P: (A \to (A \to Prop))) (f: (\forall (h1: 
+implied rec lemma leqz_ind (P: (A \to (A \to Prop))) (f: (\forall (h1: 
 nat).(\forall (h2: nat).(\forall (n1: nat).(\forall (n2: nat).((eq nat (plus 
 h1 n2) (plus h2 n1)) \to (P (ASort h1 n1) (ASort h2 n2)))))))) (f0: (\forall 
 (a1: A).(\forall (a2: A).((leqz a1 a2) \to ((P a1 a2) \to (\forall (a3: 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/leq/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/leq/fwd.ma
index 32d8e6f87..4fc6915b4 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/leq/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/leq/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/leq/defs.ma".
 
-implied let rec leq_ind (g: G) (P: (A \to (A \to Prop))) (f: (\forall (h1: 
+implied rec lemma leq_ind (g: G) (P: (A \to (A \to Prop))) (f: (\forall (h1: 
 nat).(\forall (h2: nat).(\forall (n1: nat).(\forall (n2: nat).(\forall (k: 
 nat).((eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k)) \to (P 
 (ASort h1 n1) (ASort h2 n2))))))))) (f0: (\forall (a1: A).(\forall (a2: 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma
index 6f9475944..6c5959228 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma
@@ -18,10 +18,10 @@ include "basic_1/tlist/defs.ma".
 
 include "basic_1/s/defs.ma".
 
-let rec lref_map (f: (nat \to nat)) (d: nat) (t: T) on t: T \def match t with 
-[(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i 
-d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u t0) 
-\Rightarrow (THead k (lref_map f d u) (lref_map f (s k d) t0))].
+rec definition lref_map (f: (nat \to nat)) (d: nat) (t: T) on t: T \def match 
+t with [(TSort n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match 
+(blt i d) with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k u 
+t0) \Rightarrow (THead k (lref_map f d u) (lref_map f (s k d) t0))].
 
 definition lift:
  nat \to (nat \to (T \to T))
@@ -29,7 +29,7 @@ definition lift:
  \lambda (h: nat).(\lambda (i: nat).(\lambda (t: T).(lref_map (\lambda (x: 
 nat).(plus x h)) i t))).
 
-let rec lifts (h: nat) (d: nat) (ts: TList) on ts: TList \def match ts with 
-[TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift h d t) (lifts 
-h d ts0))].
+rec definition lifts (h: nat) (d: nat) (ts: TList) on ts: TList \def match ts 
+with [TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift h d t) 
+(lifts h d ts0))].
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/lift1/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/lift1/defs.ma
index 94e6343df..4ab258905 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/lift1/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/lift1/defs.ma
@@ -16,16 +16,16 @@
 
 include "basic_1/lift/defs.ma".
 
-let rec trans (hds: PList) on hds: nat \to nat \def \lambda (i: nat).(match 
-hds with [PNil \Rightarrow i | (PCons h d hds0) \Rightarrow (let j \def 
-(trans hds0 i) in (match (blt j d) with [true \Rightarrow j | false 
+rec definition trans (hds: PList) on hds: nat \to nat \def \lambda (i: 
+nat).(match hds with [PNil \Rightarrow i | (PCons h d hds0) \Rightarrow (let 
+j \def (trans hds0 i) in (match (blt j d) with [true \Rightarrow j | false 
 \Rightarrow (plus j h)]))]).
 
-let rec lift1 (hds: PList) on hds: T \to T \def \lambda (t: T).(match hds 
-with [PNil \Rightarrow t | (PCons h d hds0) \Rightarrow (lift h d (lift1 hds0 
-t))]).
+rec definition lift1 (hds: PList) on hds: T \to T \def \lambda (t: T).(match 
+hds with [PNil \Rightarrow t | (PCons h d hds0) \Rightarrow (lift h d (lift1 
+hds0 t))]).
 
-let rec lifts1 (hds: PList) (ts: TList) on ts: TList \def match ts with [TNil 
-\Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift1 hds t) (lifts1 hds 
-ts0))].
+rec definition lifts1 (hds: PList) (ts: TList) on ts: TList \def match ts 
+with [TNil \Rightarrow TNil | (TCons t ts0) \Rightarrow (TCons (lift1 hds t) 
+(lifts1 hds ts0))].
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/llt/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/llt/defs.ma
index e1e9ee5af..7d5bc550a 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/llt/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/llt/defs.ma
@@ -16,8 +16,9 @@
 
 include "basic_1/A/defs.ma".
 
-let rec lweight (a: A) on a: nat \def match a with [(ASort _ _) \Rightarrow O 
-| (AHead a1 a2) \Rightarrow (S (plus (lweight a1) (lweight a2)))].
+rec definition lweight (a: A) on a: nat \def match a with [(ASort _ _) 
+\Rightarrow O | (AHead a1 a2) \Rightarrow (S (plus (lweight a1) (lweight 
+a2)))].
 
 definition llt:
  A \to (A \to Prop)
diff --git a/matita/matita/contribs/lambdadelta/basic_1/next_plus/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/next_plus/defs.ma
index b622b763c..04e15b3cc 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/next_plus/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/next_plus/defs.ma
@@ -16,6 +16,6 @@
 
 include "basic_1/G/defs.ma".
 
-let rec next_plus (g: G) (n: nat) (i: nat) on i: nat \def match i with [O 
-\Rightarrow n | (S i0) \Rightarrow (next g (next_plus g n i0))].
+rec definition next_plus (g: G) (n: nat) (i: nat) on i: nat \def match i with 
+[O \Rightarrow n | (S i0) \Rightarrow (next g (next_plus g n i0))].
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/nf2/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/nf2/defs.ma
index eae14f728..5b4849d7a 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/nf2/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/nf2/defs.ma
@@ -22,6 +22,6 @@ definition nf2:
  \lambda (c: C).(\lambda (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (eq T t1 
 t2)))).
 
-let rec nfs2 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil 
+rec definition nfs2 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil 
 \Rightarrow True | (TCons t ts0) \Rightarrow (land (nf2 c t) (nfs2 c ts0))].
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/pc3/left.ma b/matita/matita/contribs/lambdadelta/basic_1/pc3/left.ma
index d386b1864..579d42b24 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pc3/left.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pc3/left.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/pc3/props.ma".
 
-implied let rec pc3_left_ind (c: C) (P: (T \to (T \to Prop))) (f: (\forall 
+implied rec lemma pc3_left_ind (c: C) (P: (T \to (T \to Prop))) (f: (\forall 
 (t: T).(P t t))) (f0: (\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to 
 (\forall (t3: T).((pc3_left c t2 t3) \to ((P t2 t3) \to (P t1 t3)))))))) (f1: 
 (\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall (t3: 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/pr0/fwd.ma
index 972d92170..ad2f0e886 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pr0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pr0/fwd.ma
@@ -18,7 +18,7 @@ include "basic_1/pr0/defs.ma".
 
 include "basic_1/subst0/fwd.ma".
 
-implied let rec pr0_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t 
+implied rec lemma pr0_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t 
 t))) (f0: (\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to ((P u1 u2) \to 
 (\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to ((P t1 t2) \to (\forall 
 (k: K).(P (THead k u1 t1) (THead k u2 t2)))))))))))) (f1: (\forall (u: 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr1/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/pr1/fwd.ma
index 58b7e727f..8c9640c9f 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pr1/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pr1/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/pr1/defs.ma".
 
-implied let rec pr1_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t 
+implied rec lemma pr1_ind (P: (T \to (T \to Prop))) (f: (\forall (t: T).(P t 
 t))) (f0: (\forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: 
 T).((pr1 t2 t3) \to ((P t2 t3) \to (P t1 t3)))))))) (t: T) (t0: T) (p: pr1 t 
 t0) on p: P t t0 \def match p with [(pr1_refl t1) \Rightarrow (f t1) | 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr3/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/pr3/fwd.ma
index e3c9fca02..7f9e46419 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/pr3/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/pr3/fwd.ma
@@ -18,7 +18,7 @@ include "basic_1/pr3/defs.ma".
 
 include "basic_1/pr2/fwd.ma".
 
-implied let rec pr3_ind (c: C) (P: (T \to (T \to Prop))) (f: (\forall (t: 
+implied rec lemma pr3_ind (c: C) (P: (T \to (T \to Prop))) (f: (\forall (t: 
 T).(P t t))) (f0: (\forall (t2: T).(\forall (t1: T).((pr2 c t1 t2) \to 
 (\forall (t3: T).((pr3 c t2 t3) \to ((P t2 t3) \to (P t1 t3)))))))) (t: T) 
 (t0: T) (p: pr3 c t t0) on p: P t t0 \def match p with [(pr3_refl t1) 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/sc3/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/sc3/defs.ma
index 6a9f0739b..417868bc4 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sc3/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sc3/defs.ma
@@ -20,7 +20,7 @@ include "basic_1/arity/defs.ma".
 
 include "basic_1/drop1/defs.ma".
 
-let rec sc3 (g: G) (a: A) on a: C \to (T \to Prop) \def \lambda (c: 
+rec definition sc3 (g: G) (a: A) on a: C \to (T \to Prop) \def \lambda (c: 
 C).(\lambda (t: T).(match a with [(ASort h n) \Rightarrow (land (arity g c t 
 (ASort h n)) (sn3 c t)) | (AHead a1 a2) \Rightarrow (land (arity g c t (AHead 
 a1 a2)) (\forall (d: C).(\forall (w: T).((sc3 g a1 d w) \to (\forall (is: 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
index c6980318b..d9ba6092c 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sn3/defs.ma
@@ -20,6 +20,6 @@ inductive sn3 (c: C): T \to Prop \def
 | sn3_sing: \forall (t1: T).(((\forall (t2: T).((((eq T t1 t2) \to (\forall 
 (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2))))) \to (sn3 c t1)).
 
-let rec sns3 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil 
+rec definition sns3 (c: C) (ts: TList) on ts: Prop \def match ts with [TNil 
 \Rightarrow True | (TCons t ts0) \Rightarrow (land (sn3 c t) (sns3 c ts0))].
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/sn3/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/sn3/fwd.ma
index 2550405f2..fe603b59c 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sn3/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sn3/fwd.ma
@@ -18,7 +18,7 @@ include "basic_1/sn3/defs.ma".
 
 include "basic_1/pr3/props.ma".
 
-implied let rec sn3_ind (c: C) (P: (T \to Prop)) (f: (\forall (t1: 
+implied rec lemma sn3_ind (c: C) (P: (T \to Prop)) (f: (\forall (t1: 
 T).(((\forall (t2: T).((((eq T t1 t2) \to (\forall (P0: Prop).P0))) \to ((pr3 
 c t1 t2) \to (sn3 c t2))))) \to (((\forall (t2: T).((((eq T t1 t2) \to 
 (\forall (P0: Prop).P0))) \to ((pr3 c t1 t2) \to (P t2))))) \to (P t1))))) 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
index 5b80b01a2..0d05ca147 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/sty0/defs.ma".
 
-implied let rec sty0_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f: 
+implied rec lemma sty0_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f: 
 (\forall (c: C).(\forall (n: nat).(P c (TSort n) (TSort (next g n)))))) (f0: 
 (\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c 
 (CHead d (Bind Abbr) v)) \to (\forall (w: T).((sty0 g d v w) \to ((P d v w) 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty1/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/sty1/fwd.ma
index 535f3ff11..7307b49ff 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sty1/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty1/fwd.ma
@@ -16,10 +16,10 @@
 
 include "basic_1/sty1/defs.ma".
 
-implied let rec sty1_ind (g: G) (c: C) (t1: T) (P: (T \to Prop)) (f: (\forall 
-(t2: T).((sty0 g c t1 t2) \to (P t2)))) (f0: (\forall (t: T).((sty1 g c t1 t) 
-\to ((P t) \to (\forall (t2: T).((sty0 g c t t2) \to (P t2))))))) (t: T) (s0: 
-sty1 g c t1 t) on s0: P t \def match s0 with [(sty1_sty0 t2 s1) \Rightarrow 
-(f t2 s1) | (sty1_sing t0 s1 t2 s2) \Rightarrow (f0 t0 s1 ((sty1_ind g c t1 P 
-f f0) t0 s1) t2 s2)].
+implied rec lemma sty1_ind (g: G) (c: C) (t1: T) (P: (T \to Prop)) (f: 
+(\forall (t2: T).((sty0 g c t1 t2) \to (P t2)))) (f0: (\forall (t: T).((sty1 
+g c t1 t) \to ((P t) \to (\forall (t2: T).((sty0 g c t t2) \to (P t2))))))) 
+(t: T) (s0: sty1 g c t1 t) on s0: P t \def match s0 with [(sty1_sty0 t2 s1) 
+\Rightarrow (f t2 s1) | (sty1_sing t0 s1 t2 s2) \Rightarrow (f0 t0 s1 
+((sty1_ind g c t1 P f f0) t0 s1) t2 s2)].
 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/subst/defs.ma
index bf89e1618..8d9ed5f07 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/subst/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/subst/defs.ma
@@ -16,8 +16,8 @@
 
 include "basic_1/lift/defs.ma".
 
-let rec subst (d: nat) (v: T) (t: T) on t: T \def match t with [(TSort n) 
-\Rightarrow (TSort n) | (TLRef i) \Rightarrow (match (blt i d) with [true 
+rec definition subst (d: nat) (v: T) (t: T) on t: T \def match t with [(TSort 
+n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (match (blt i d) with [true 
 \Rightarrow (TLRef i) | false \Rightarrow (match (blt d i) with [true 
 \Rightarrow (TLRef (pred i)) | false \Rightarrow (lift d O v)])]) | (THead k 
 u t0) \Rightarrow (THead k (subst d v u) (subst (s k d) v t0))].
diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/subst0/fwd.ma
index 5af139ab0..930835ccb 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/subst0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/subst0/fwd.ma
@@ -18,7 +18,7 @@ include "basic_1/subst0/defs.ma".
 
 include "basic_1/lift/fwd.ma".
 
-implied let rec subst0_ind (P: (nat \to (T \to (T \to (T \to Prop))))) (f: 
+implied rec lemma subst0_ind (P: (nat \to (T \to (T \to (T \to Prop))))) (f: 
 (\forall (v: T).(\forall (i: nat).(P i v (TLRef i) (lift (S i) O v))))) (f0: 
 (\forall (v: T).(\forall (u2: T).(\forall (u1: T).(\forall (i: nat).((subst0 
 i v u1 u2) \to ((P i v u1 u2) \to (\forall (t: T).(\forall (k: K).(P i v 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlist/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/tlist/defs.ma
index 86b88b5df..d0eed7f52 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/tlist/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/tlist/defs.ma
@@ -20,16 +20,16 @@ inductive TList: Type[0] \def
 | TNil: TList
 | TCons: T \to (TList \to TList).
 
-let rec THeads (k: K) (us: TList) on us: T \to T \def \lambda (t: T).(match 
-us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u (THeads k 
-ul t))]).
+rec definition THeads (k: K) (us: TList) on us: T \to T \def \lambda (t: 
+T).(match us with [TNil \Rightarrow t | (TCons u ul) \Rightarrow (THead k u 
+(THeads k ul t))]).
 
-let rec TApp (ts: TList) on ts: T \to TList \def \lambda (v: T).(match ts 
-with [TNil \Rightarrow (TCons v TNil) | (TCons t ts0) \Rightarrow (TCons t 
+rec definition TApp (ts: TList) on ts: T \to TList \def \lambda (v: T).(match 
+ts with [TNil \Rightarrow (TCons v TNil) | (TCons t ts0) \Rightarrow (TCons t 
 (TApp ts0 v))]).
 
-let rec tslen (ts: TList) on ts: nat \def match ts with [TNil \Rightarrow O | 
-(TCons _ ts0) \Rightarrow (S (tslen ts0))].
+rec definition tslen (ts: TList) on ts: nat \def match ts with [TNil 
+\Rightarrow O | (TCons _ ts0) \Rightarrow (S (tslen ts0))].
 
 definition tslt:
  TList \to (TList \to Prop)
diff --git a/matita/matita/contribs/lambdadelta/basic_1/tlt/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/tlt/defs.ma
index 3a21225f2..174740042 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/tlt/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/tlt/defs.ma
@@ -22,8 +22,8 @@ definition wadd:
  \lambda (f: ((nat \to nat))).(\lambda (w: nat).(\lambda (n: nat).(match n 
 with [O \Rightarrow w | (S m) \Rightarrow (f m)]))).
 
-let rec weight_map (f: (nat \to nat)) (t: T) on t: nat \def match t with 
-[(TSort _) \Rightarrow O | (TLRef n) \Rightarrow (f n) | (THead k u t0) 
+rec definition weight_map (f: (nat \to nat)) (t: T) on t: nat \def match t 
+with [(TSort _) \Rightarrow O | (TLRef n) \Rightarrow (f n) | (THead k u t0) 
 \Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr 
 \Rightarrow (S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f 
 u))) t0))) | Abst \Rightarrow (S (plus (weight_map f u) (weight_map (wadd f 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/ty3/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/ty3/fwd.ma
index 13e8ec9ac..318a97986 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/ty3/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ty3/fwd.ma
@@ -18,14 +18,14 @@ include "basic_1/ty3/defs.ma".
 
 include "basic_1/pc3/props.ma".
 
-implied let rec ty3_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f: (\forall 
-(c: C).(\forall (t2: T).(\forall (t: T).((ty3 g c t2 t) \to ((P c t2 t) \to 
-(\forall (u: T).(\forall (t1: T).((ty3 g c u t1) \to ((P c u t1) \to ((pc3 c 
-t1 t2) \to (P c u t2)))))))))))) (f0: (\forall (c: C).(\forall (m: nat).(P c 
-(TSort m) (TSort (next g m)))))) (f1: (\forall (n: nat).(\forall (c: 
-C).(\forall (d: C).(\forall (u: T).((getl n c (CHead d (Bind Abbr) u)) \to 
-(\forall (t: T).((ty3 g d u t) \to ((P d u t) \to (P c (TLRef n) (lift (S n) 
-O t))))))))))) (f2: (\forall (n: nat).(\forall (c: C).(\forall (d: 
+implied rec lemma ty3_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f: 
+(\forall (c: C).(\forall (t2: T).(\forall (t: T).((ty3 g c t2 t) \to ((P c t2 
+t) \to (\forall (u: T).(\forall (t1: T).((ty3 g c u t1) \to ((P c u t1) \to 
+((pc3 c t1 t2) \to (P c u t2)))))))))))) (f0: (\forall (c: C).(\forall (m: 
+nat).(P c (TSort m) (TSort (next g m)))))) (f1: (\forall (n: nat).(\forall 
+(c: C).(\forall (d: C).(\forall (u: T).((getl n c (CHead d (Bind Abbr) u)) 
+\to (\forall (t: T).((ty3 g d u t) \to ((P d u t) \to (P c (TLRef n) (lift (S 
+n) O t))))))))))) (f2: (\forall (n: nat).(\forall (c: C).(\forall (d: 
 C).(\forall (u: T).((getl n c (CHead d (Bind Abst) u)) \to (\forall (t: 
 T).((ty3 g d u t) \to ((P d u t) \to (P c (TLRef n) (lift (S n) O 
 u))))))))))) (f3: (\forall (c: C).(\forall (u: T).(\forall (t: T).((ty3 g c u 
@@ -54,7 +54,7 @@ t3 t4 ((ty3_ind g P f f0 f1 f2 f3 f4 f5) c0 v (THead (Bind Abst) u t3) t4)) |
 f1 f2 f3 f4 f5) c0 t2 t3 t4) t5 t6 ((ty3_ind g P f f0 f1 f2 f3 f4 f5) c0 t3 
 t5 t6))].
 
-implied let rec tys3_ind (g: G) (c: C) (P: (TList \to (T \to Prop))) (f: 
+implied rec lemma tys3_ind (g: G) (c: C) (P: (TList \to (T \to Prop))) (f: 
 (\forall (u: T).(\forall (u0: T).((ty3 g c u u0) \to (P TNil u))))) (f0: 
 (\forall (t: T).(\forall (u: T).((ty3 g c t u) \to (\forall (ts: 
 TList).((tys3 g c ts u) \to ((P ts u) \to (P (TCons t ts) u)))))))) (t: 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/wcpr0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/wcpr0/fwd.ma
index 4f6e1df9f..8d4ccb52e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/wcpr0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/wcpr0/fwd.ma
@@ -16,13 +16,13 @@
 
 include "basic_1/wcpr0/defs.ma".
 
-implied let rec wcpr0_ind (P: (C \to (C \to Prop))) (f: (\forall (c: C).(P c 
-c))) (f0: (\forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to ((P c1 c2) \to 
-(\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (k: K).(P (CHead 
-c1 k u1) (CHead c2 k u2))))))))))) (c: C) (c0: C) (w: wcpr0 c c0) on w: P c 
-c0 \def match w with [(wcpr0_refl c1) \Rightarrow (f c1) | (wcpr0_comp c1 c2 
-w0 u1 u2 p k) \Rightarrow (f0 c1 c2 w0 ((wcpr0_ind P f f0) c1 c2 w0) u1 u2 p 
-k)].
+implied rec lemma wcpr0_ind (P: (C \to (C \to Prop))) (f: (\forall (c: C).(P 
+c c))) (f0: (\forall (c1: C).(\forall (c2: C).((wcpr0 c1 c2) \to ((P c1 c2) 
+\to (\forall (u1: T).(\forall (u2: T).((pr0 u1 u2) \to (\forall (k: K).(P 
+(CHead c1 k u1) (CHead c2 k u2))))))))))) (c: C) (c0: C) (w: wcpr0 c c0) on 
+w: P c c0 \def match w with [(wcpr0_refl c1) \Rightarrow (f c1) | (wcpr0_comp 
+c1 c2 w0 u1 u2 p k) \Rightarrow (f0 c1 c2 w0 ((wcpr0_ind P f f0) c1 c2 w0) u1 
+u2 p k)].
 
 lemma wcpr0_gen_sort:
  \forall (x: C).(\forall (n: nat).((wcpr0 (CSort n) x) \to (eq C x (CSort 
diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma
index 98eb5558c..d4718ec6e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma
@@ -16,7 +16,7 @@
 
 include "basic_1/wf3/defs.ma".
 
-implied let rec wf3_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (m: 
+implied rec lemma wf3_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (m: 
 nat).(P (CSort m) (CSort m)))) (f0: (\forall (c1: C).(\forall (c2: C).((wf3 g 
 c1 c2) \to ((P c1 c2) \to (\forall (u: T).(\forall (t: T).((ty3 g c1 u t) \to 
 (\forall (b: B).(P (CHead c1 (Bind b) u) (CHead c2 (Bind b) u))))))))))) (f1: 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/blt/defs.ma b/matita/matita/contribs/lambdadelta/ground_1/blt/defs.ma
index f1eee61f5..3b8f8656e 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/blt/defs.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/blt/defs.ma
@@ -16,7 +16,7 @@
 
 include "ground_1/preamble.ma".
 
-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)])].
+rec definition 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)])].
 
diff --git a/matita/matita/contribs/lambdadelta/ground_1/plist/defs.ma b/matita/matita/contribs/lambdadelta/ground_1/plist/defs.ma
index cfb67e1ff..13a7bd07a 100644
--- a/matita/matita/contribs/lambdadelta/ground_1/plist/defs.ma
+++ b/matita/matita/contribs/lambdadelta/ground_1/plist/defs.ma
@@ -20,14 +20,15 @@ inductive PList: Type[0] \def
 | PNil: PList
 | PCons: nat \to (nat \to (PList \to PList)).
 
-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))])).
+rec definition 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))])).
 
-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))].
+rec definition Ss (hds: PList) on hds: PList \def match hds with [PNil 
+\Rightarrow PNil | (PCons h d hds0) \Rightarrow (PCons h (S d) (Ss hds0))].
 
-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))]).
+rec definition 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/legacy_1/coq/defs.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
index 75e58b036..497403d32 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
@@ -68,12 +68,12 @@ definition pred:
 \def
  \lambda (n: nat).(match n with [O \Rightarrow O | (S u) \Rightarrow u]).
 
-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))]).
+rec definition 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))]).
 
-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)])]).
+rec definition 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: 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 
diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
index 8f5ee7307..c11c7d732 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
@@ -81,12 +81,12 @@ implied lemma eq_ind:
  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(eq_rect A 
 x P))).
 
-implied let rec le_ind (n: nat) (P: (nat \to Prop)) (f: P n) (f0: (\forall 
+implied rec lemma 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 with [le_n \Rightarrow f | (le_S m l0) \Rightarrow (f0 m l0 
 ((le_ind n P f f0) m l0))].
 
-implied let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to 
+implied rec lemma 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 with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda 
-- 
2.39.2