From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 24 Jul 2011 12:23:53 +0000 (+0000)
Subject: - sone refactoring
X-Git-Tag: make_still_working~2353
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f29b61aeae23efb412ac48ab747d63bcedcacd6;p=helm.git

- sone refactoring
- notation fix
- telescopic substitution replaced by parallel substitution
- context-free parallel reduction added
---

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 97c45196a..d39b3faf4 100644
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -12,7 +12,6 @@
 include "basics/list.ma".
 include "lambda-delta/xoa_defs.ma".
 include "lambda-delta/xoa_notation.ma".
-include "lambda-delta/notation.ma".
 
 (* ARITHMETICAL PROPERTIES **************************************************)
 
diff --git a/matita/matita/lib/lambda-delta/notation.ma b/matita/matita/lib/lambda-delta/notation.ma
index 79fcc3a97..6f883cc71 100644
--- a/matita/matita/lib/lambda-delta/notation.ma
+++ b/matita/matita/lib/lambda-delta/notation.ma
@@ -17,7 +17,7 @@ notation "hvbox( ⋆ )"
  non associative with precedence 90
  for @{ 'Star }.
 
-notation "hvbox( ⋆ k )"
+notation "hvbox( ⋆ term 90 k )"
  non associative with precedence 90
  for @{ 'Star $k }.
 
@@ -53,18 +53,18 @@ notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )"
 
 notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )"
    non associative with precedence 45
-   for @{ 'RSubst $L1 $d $e $L2 }.
+   for @{ 'RDrop $L1 $d $e $L2 }.
 
-notation "hvbox( L ⊢ break ↓ [ d , break e ] break T1 ≡ break T2 )"
+notation "hvbox( L ⊢ break (term 90 T1) break [ d , break e ] ≫ break T2 )"
    non associative with precedence 45
-   for @{ 'RSubst $L $T1 $d $e $T2 }.
+   for @{ 'PSubst $L $T1 $d $e $T2 }.
 
 (* reduction ****************************************************************)
 
 notation "hvbox( T1 ⇒ break T2 )"
    non associative with precedence 45
-   for @{ 'PR $T1 $T2 }.
+   for @{ 'PRed $T1 $T2 }.
 
 notation "hvbox( L ⊢ break (term 90 T1) ⇒ break T2 )"
    non associative with precedence 45
-   for @{ 'PR $L $T1 $T2 }.
+   for @{ 'PRed $L $T1 $T2 }.
diff --git a/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
new file mode 100644
index 000000000..dab96f2dd
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "lambda-delta/reduction/tpr_defs.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+inductive lpr: lenv → lenv → Prop ≝
+| lpr_sort: lpr (⋆) (⋆)
+| lpr_item: ∀K1,K2,I,V1,V2.
+            lpr K1 K2 → V1 ⇒ V2 → lpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
+.
+
+interpretation
+  "context-free parallel reduction (environment)"
+  'PR L1 L2 = (lpr L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
+                         ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+#L1 #L2 #H elim H -H L1 L2
+[ #K1 #I #V1 #H destruct
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #_ #L #J #W #H destruct - K1 I V1 /2 width=5/
+]
+qed.
+
+lemma lpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 →
+                     ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/reduction/pr_defs.ma b/matita/matita/lib/lambda-delta/reduction/pr_defs.ma
deleted file mode 100644
index d45cbd0d8..000000000
--- a/matita/matita/lib/lambda-delta/reduction/pr_defs.ma
+++ /dev/null
@@ -1,81 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/substitution/drop_defs.ma".
-
-(* SINGLE STEP PARALLEL REDUCTION ON TERMS **********************************)
-
-inductive pr: lenv → term → term → Prop ≝
-| pr_sort : ∀L,k. pr L (⋆k) (⋆k)
-| pr_lref : ∀L,i. pr L (#i) (#i)
-| pr_bind : ∀L,I,V1,V2,T1,T2. pr L V1 V2 → pr (L. 𝕓{I} V1) T1 T2 →
-            pr L (𝕓{I} V1. T1) (𝕓{I} V2. T2)
-| pr_flat : ∀L,I,V1,V2,T1,T2. pr L V1 V2 → pr L T1 T2 →
-            pr L (𝕗{I} V1. T1) (𝕗{I} V2. T2)
-| pr_beta : ∀L,V1,V2,W,T1,T2.
-            pr L V1 V2 → pr (L. 𝕓{Abst} W) T1 T2 → (*𝕓*)
-            pr L (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2)
-| pr_delta: ∀L,K,V1,V2,V,i.
-            ↑[0,i] K. 𝕓{Abbr} V1 ≡ L → pr K V1 V2 → ↑[0,i+1] V2 ≡ V →
-            pr L (#i) V
-| pr_theta: ∀L,V,V1,V2,W1,W2,T1,T2.
-            pr L V1 V2 → ↑[0,1] V2 ≡ V → pr L W1 W2 → pr (L. 𝕓{Abbr} W1) T1 T2 → (*𝕓*)
-            pr L (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2)
-| pr_zeta : ∀L,V,T,T1,T2. ↑[0,1] T1 ≡ T → pr L T1 T2 →
-            pr L (𝕚{Abbr} V. T) T2
-| pr_tau  : ∀L,V,T1,T2. pr L T1 T2 → pr L (𝕚{Cast} V. T1) T2
-.
-
-interpretation
-   "single step parallel reduction (term)"
-   'PR L T1 T2 = (pr L T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma pr_refl: ∀T,L. L ⊢ T ⇒ T.
-#T elim T -T //
-#I elim I -I /2/
-qed.
-
-(* The basic inversion lemmas ***********************************************)
-
-lemma pr_inv_lref2_aux: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → ∀i. T2 = #i →
-                        ∨∨           T1 = #i
-                         | ∃∃K,V1,j. j < i & K ⊢ V1 ⇒ #(i-j-1) &
-                                     ↑[O,j] K. 𝕓{Abbr} V1 ≡ L & T1 = #j
-                         | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & L ⊢ T0 ⇒ #i &
-                                     T1 = 𝕓{Abbr} V. T
-                         | ∃∃V,T.    L ⊢ T ⇒ #i & T1 = 𝕗{Cast} V. T.
-#L #T1 #T2 #H elim H -H L T1 T2
-[ #L #k #i #H destruct
-| #L #j #i /2/
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #L #K #V1 #V2 #V #j #HLK #HV12 #HV2 #_ #i #H destruct -V;
-  elim (lift_inv_lref2 … HV2) -HV2 * #H1 #H2
-  [ elim (lt_zero_false … H1)
-  | destruct -V2 /3 width=7/
-  ]
-| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct
-| #L #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/
-| #L #V #T1 #T2 #HT12 #_ #i #H destruct /3/
-]
-qed.
-
-lemma pr_inv_lref2: ∀L,T1,i. L ⊢ T1 ⇒ #i →
-                    ∨∨           T1 = #i
-                     | ∃∃K,V1,j. j < i & K ⊢ V1 ⇒ #(i-j-1) &
-                                 ↑[O,j] K. 𝕓{Abbr} V1 ≡ L & T1 = #j
-                     | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & L ⊢ T0 ⇒ #i &
-                                 T1 = 𝕓{Abbr} V. T
-                     | ∃∃V,T.    L ⊢ T ⇒ #i & T1 = 𝕗{Cast} V. T.
-/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/reduction/pr_pr.ma b/matita/matita/lib/lambda-delta/reduction/pr_pr.ma
index fc284e06d..c8942bea2 100644
--- a/matita/matita/lib/lambda-delta/reduction/pr_pr.ma
+++ b/matita/matita/lib/lambda-delta/reduction/pr_pr.ma
@@ -22,6 +22,20 @@ lemma pr_conf_sort_sort: ∀L,k1. ∃∃T0. L ⊢ (⋆k1) ⇒ T0 & L ⊢ (⋆k1)
 lemma pr_conf_lref_lref: ∀L,i1. ∃∃T0. L ⊢ (#i1) ⇒ T0 & L ⊢ (#i1) ⇒ T0.
 /2/ qed.
 
+lemma pr_conf_bind_bind:
+   ∀L,I1,V11,V12,T11,T12,V22,T22. (
+      ∀L1,T1. #L1 + #T1 < #L + (#V11 + #T11 + 1) →
+      ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 →
+      ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0
+   ) →
+   L ⊢ V11 ⇒ V12 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T12 →
+   L ⊢ V11 ⇒ V22 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T22 →
+   ∃∃T0. L ⊢ 𝕓{I1} V12. T12 ⇒ T0 & L ⊢ 𝕓{I1} V22. T22 ⇒ T0.
+#L #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
+elim (IH … HV1 … HV2) [2: /2/ ] #V #HV1 #HV2
+elim (IH … HT1 … HT2) [2: normalize // ] -HT1 HT2 T11 IH #T #HT1 #HT2
+@ex2_1_intro [2: @pr_bind [3: @HV1 |1: skip |4: 
+
 (* Confluence ***************************************************************)
 
 lemma pr_conf_aux:
@@ -37,7 +51,7 @@ lemma pr_conf_aux:
 * -K1 U1 T1
 [ #K1 #k1 * -K2 U2 T2
 (* case 1: sort, sort *)
-  [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -K1 K2 T k2 IH //
+  [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -K1 K2 T k2 //
 (* case 2: sort, lref (excluded) *)
   | #K2 #i2 #H1 #H2 #H3 #H4 destruct
 (* case 3: sort, bind (excluded) *)
@@ -56,10 +70,10 @@ lemma pr_conf_aux:
   | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct
   ]
 | #K1 #i1 * -K2 U2 T2
-(* case 10: lref, sort (excluded) *)
+(* case 10: lref, sort (excluded) broken *)
   [ #K2 #k2 #H1 #H2 #H3 #H4 destruct
 (* case 11: lref, sort (excluded) *)
-  | #K2 #i2 #H1 #H2 #H3 #H4 destruct -K1 K2 T i2 IH //
+  | #K2 #i2 #H1 #H2 #H3 #H4 destruct -K1 K2 T i2 //
 (* case 12: lref, bind (excluded) *)
   | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
 (* case 13: lref, flat (excluded) *)
@@ -74,11 +88,28 @@ lemma pr_conf_aux:
   | #K2 #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 #H3 #H4 destruct
 (* case 18: lref, tau (excluded) *)
   | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct
-  ]  
+  ]
+| #K1 #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -K2 U2 T2
+(* case 19: bind, sort (excluded) broken *)
+  [ #K2 #k2 #H1 #H2 #H3 #H4 destruct
+(* case 20: bind, lref (excluded) *)
+  | #K2 #i2 #H1 #H2 #H3 #H4 destruct
+(* case 21: bind, bind *)
+  | #K2 #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2 #H3 #H4
+    destruct -T K1 K2 I2 V21 T21;
+
 
 theorem pr_conf: ∀L,T,T1,T2. L ⊢ T ⇒ T1 → L ⊢ T ⇒ T2 →
                  ∃∃T0. L ⊢ T1 ⇒ T0 & L ⊢ T2 ⇒ T0.
 #L #T @(cw_wf_ind … L T) -L T /3 width=12/
 qed.
 
-
+lemma pr_conf_bind_bind:
+   ∀L,I1,V11,V12,T11,T12,V22,T22. (
+      ∀L1,T1. #L1 + #T1 < #L + (#V11 + #T11 + 1) →
+      ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 →
+      ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0
+   ) →
+   L ⊢ V11 ⇒ V12 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T12 →
+   L ⊢ V11 ⇒ V22 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T22 →
+   ∃∃T0. L ⊢ 𝕓{I1} V12. T12 ⇒ T0 & L ⊢ 𝕓{I1} V22. T22 ⇒ T0.
diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
new file mode 100644
index 000000000..29f8ae4e7
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
@@ -0,0 +1,74 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/substitution/subst_defs.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+inductive tpr: term → term → Prop ≝
+| tpr_sort : ∀k. tpr (⋆k) (⋆k)
+| tpr_lref : ∀i. tpr (#i) (#i)
+| tpr_bind : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
+             tpr (𝕓{I} V1. T1) (𝕓{I} V2. T2)
+| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
+             tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
+| tpr_beta : ∀V1,V2,W,T1,T2.
+             tpr V1 V2 → tpr T1 T2 →
+             tpr (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2)
+| tpr_delta: ∀V1,V2,T1,T2,T0,T.
+             tpr V1 V2 → tpr T1 T2 →
+             ⋆.  𝕓{Abbr} V2 ⊢ ↓[0, 1] T2 ≡ T0 → ↑[0, 1] T0 ≡ T →
+             tpr (𝕚{Abbr} V1. T1) (𝕚{Abbr} V2. T)
+| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
+             tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
+             tpr (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2)
+| tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 →
+             tpr (𝕚{Abbr} V. T) T2
+| tpr_tau  : ∀V,T1,T2. tpr T1 T2 → tpr (𝕚{Cast} V. T1) T2
+.
+
+interpretation
+   "context-free parallel reduction (term)"
+   'PR T1 T2 = (tpr T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma tpr_refl: ∀T. T ⇒ T.
+#T elim T -T //
+#I elim I -I /2/
+qed.
+
+(* The basic inversion lemmas ***********************************************)
+
+lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
+                         ∨∨           T1 = #i
+                          | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
+                                      T1 = 𝕓{Abbr} V. T
+                          | ∃∃V,T.    T ⇒ #i & T1 = 𝕗{Cast} V. T.
+#T1 #T2 #H elim H -H T1 T2
+[ #k #i #H destruct
+| #j #i /2/
+| #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #V1 #V2 #T1 #T2 #T0 #T #_ #_ #_ #_ #_ #_ #i #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct
+| #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/
+| #V #T1 #T2 #HT12 #_ #i #H destruct /3/
+]
+qed.
+
+lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
+                     ∨∨           T1 = #i
+                      | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
+                                  T1 = 𝕓{Abbr} V. T
+                      | ∃∃V,T.    T ⇒ #i & T1 = 𝕗{Cast} V. T.
+/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
index 623467dd5..1bf8e278d 100644
--- a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
@@ -22,19 +22,19 @@ inductive drop: lenv → nat → nat → lenv → Prop ≝
              drop (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2)
 .
 
-interpretation "dropping" 'RLift L2 d e L1 = (drop L1 d e L2).
+interpretation "dropping" 'RDrop L1 d e L2 = (drop L1 d e L2).
 
 (* Basic properties *********************************************************) 
 
 lemma drop_drop_lt: ∀L1,L2,I,V,e. 
-                    ↑[0, e - 1] L2 ≡ L1 → 0 < e → ↑[0, e] L2 ≡ L1. 𝕓{I} V.
+                    ↓[0, e - 1] L1 ≡ L2 → 0 < e → ↓[0, e] L1. 𝕓{I} V ≡ L2.
 #L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma drop_inv_refl_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 → e = 0 → L1 = L2.
-#d #e #L2 #L1 #H elim H -H d e L2 L1
+lemma drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2.
+#d #e #L1 #L2 #H elim H -H d e L1 L2
 [ //
 | #L1 #L2 #I #V #e #_ #_ #_ #H
   elim (plus_S_eq_O_false … H)
@@ -43,35 +43,35 @@ lemma drop_inv_refl_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 → e = 0 
 ]
 qed.
 
-lemma drop_inv_refl: ∀L2,L1. ↑[0, 0] L2 ≡ L1 → L1 = L2.
+lemma drop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2.
 /2 width=5/ qed.
 
-lemma drop_inv_O1_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 →
+lemma drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 →
                        ∀K,I,V. L1 = K. 𝕓{I} V → 
                        (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
-                       (0 < e ∧ ↑[d, e - 1] L2 ≡ K).
-#d #e #L2 #L1 #H elim H -H d e L2 L1
+                       (0 < e ∧ ↓[d, e - 1] K ≡ L2).
+#d #e #L1 #L2 #H elim H -H d e L1 L2
 [ /3/
 | #L1 #L2 #I #V #e #HL12 #_ #_ #K #J #W #H destruct -L1 I V /3/
 | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #H elim (plus_S_eq_O_false … H)
 ]
 qed.
 
-lemma drop_inv_O1: ∀e,L2,K,I,V. ↑[0, e] L2 ≡ K. 𝕓{I} V →
+lemma drop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 →
                    (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
-                   (0 < e ∧ ↑[0, e - 1] L2 ≡ K).
+                   (0 < e ∧ ↓[0, e - 1] K ≡ L2).
 /2/ qed.
 
-lemma drop_inv_drop1: ∀e,L2,K,I,V.
-                      ↑[0, e] L2 ≡ K. 𝕓{I} V → 0 < e → ↑[0, e - 1] L2 ≡ K.
-#e #L2 #K #I #V #H #He
+lemma drop_inv_drop1: ∀e,K,I,V,L2.
+                      ↓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ↓[0, e - 1] K ≡ L2.
+#e #K #I #V #L2 #H #He
 elim (drop_inv_O1 … H) -H * // #H destruct -e;
 elim (lt_refl_false … He)
 qed.
 
-lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↑[d, e] L2 ≡ L1 → 0 < d →
+lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
                           ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
-                          ∃∃K1,V1. ↑[d - 1, e] K2 ≡ K1 &
+                          ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 &
                                    ↑[d - 1, e] V2 ≡ V1 & 
                                    L1 = K1. 𝕓{I} V1.
 #d #e #L1 #L2 #H elim H -H d e L1 L2
@@ -82,7 +82,7 @@ lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↑[d, e] L2 ≡ L1 → 0 < d →
 ]
 qed.
 
-lemma drop_inv_skip2: ∀d,e,I,L1,K2,V2. ↑[d, e] K2. 𝕓{I} V2 ≡ L1 → 0 < d →
-                      ∃∃K1,V1. ↑[d - 1, e] K2 ≡ K1 & ↑[d - 1, e] V2 ≡ V1 &
+lemma drop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d →
+                      ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 &
                                L1 = K1. 𝕓{I} V1.
 /2/ qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/drop_main.ma b/matita/matita/lib/lambda-delta/substitution/drop_main.ma
index 4665b770c..a305b78c7 100644
--- a/matita/matita/lib/lambda-delta/substitution/drop_main.ma
+++ b/matita/matita/lib/lambda-delta/substitution/drop_main.ma
@@ -18,9 +18,9 @@ include "lambda-delta/substitution/drop_defs.ma".
 
 (* the main properties ******************************************************)
 
-lemma drop_conf_ge: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
-                    ∀e2,L2. ↑[0, e2] L2 ≡ L → d1 + e1 ≤ e2 →
-                    ↑[0, e2 - e1] L2 ≡ L1.
+lemma drop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 →
+                    ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 →
+                    ↓[0, e2 - e1] L1 ≡ L2.
 #d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
 [ //
 | #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
@@ -34,11 +34,11 @@ lemma drop_conf_ge: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
 ]
 qed.
 
-lemma drop_conf_lt: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
-                    ∀e2,K2,I,V2. ↑[0, e2] K2. 𝕓{I} V2 ≡ L →
+lemma drop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 →
+                    ∀e2,K2,I,V2. ↓[0, e2] L ≡ K2. 𝕓{I} V2 →
                     e2 < d1 → let d ≝ d1 - e2 - 1 in
-                    ∃∃K1,V1. ↑[0, e2] K1. 𝕓{I} V1 ≡ L1 & 
-                             ↑[d, e1] K1 ≡ K2 & ↑[d,e1] V1 ≡ V2.
+                    ∃∃K1,V1. ↓[0, e2] L1 ≡ K1. 𝕓{I} V1 &
+                             ↓[d, e1] K2 ≡ K1 & ↑[d, e1] V1 ≡ V2.
 #d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
 [ #L0 #e2 #K2 #I #V2 #_ #H
   elim (lt_zero_false … H)
@@ -53,9 +53,9 @@ lemma drop_conf_lt: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
 ]
 qed.
 
-lemma drop_trans_le: ∀d1,e1,L1. ∀L:lenv. ↑[d1, e1] L ≡ L1 →
-                     ∀e2,L2. ↑[0, e2] L2 ≡ L → e2 ≤ d1 →
-                     ∃∃L0. ↑[0, e2] L0 ≡ L1 & ↑[d1 - e2, e1] L2 ≡ L0.
+lemma drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
+                     ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 →
+                     ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2.
 #d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
 [ #L #e2 #L2 #HL2 #H
   lapply (le_O_to_eq_O … H) -H #H destruct -e2 /2/
@@ -73,8 +73,8 @@ lemma drop_trans_le: ∀d1,e1,L1. ∀L:lenv. ↑[d1, e1] L ≡ L1 →
 ]
 qed.
 
-lemma drop_trans_ge: ∀d1,e1,L1,L. ↑[d1, e1] L ≡ L1 →
-                     ∀e2,L2. ↑[0, e2] L2 ≡ L → d1 ≤ e2 → ↑[0, e1 + e2] L2 ≡ L1.
+lemma drop_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
+                     ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2.
 #d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
 [ //
 | /3/
@@ -86,5 +86,5 @@ lemma drop_trans_ge: ∀d1,e1,L1,L. ↑[d1, e1] L ≡ L1 →
 ]
 qed.
 
-axiom drop_div: ∀e1,L1. ∀L:lenv. ↑[0, e1] L ≡ L1 → ∀e2,L2. ↑[0, e2] L ≡ L2 →
-                ∃∃L0. ↑[0, e1] L2 ≡ L0 & ↑[e1, e2] L1 ≡ L0.
+axiom drop_div: ∀e1,L1,L. ↓[0, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L2 ≡ L →
+                ∃∃L0. ↓[0, e1] L0 ≡ L2 & ↓[e1, e2] L0 ≡ L1.
diff --git a/matita/matita/lib/lambda-delta/substitution/psubst_defs.ma b/matita/matita/lib/lambda-delta/substitution/psubst_defs.ma
new file mode 100644
index 000000000..514e0ad2e
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/substitution/psubst_defs.ma
@@ -0,0 +1,78 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/substitution/drop_defs.ma".
+
+(* PARALLEL SUBSTITUTION ****************************************************)
+
+inductive ps: lenv → term → nat → nat → term → Prop ≝
+| ps_sort : ∀L,k,d,e. ps L (⋆k) d e (⋆k)
+| ps_lref : ∀L,i,d,e. ps L (#i) d e (#i)
+| ps_subst: ∀L,K,V,U1,U2,i,d,e.
+            d ≤ i → i < d + e →
+            ↓[0, i] L ≡ K. 𝕓{Abbr} V → ps K V 0 (d + e - i - 1) U1 →
+            ↑[0, i + 1] U1 ≡ U2 → ps L (#i) d e U2
+| ps_bind : ∀L,I,V1,V2,T1,T2,d,e.
+            ps L V1 d e V2 → ps (L. 𝕓{I} V1) T1 (d + 1) e T2 →
+            ps L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
+| ps_flat : ∀L,I,V1,V2,T1,T2,d,e.
+            ps L V1 d e V2 → ps L T1 d e T2 →
+            ps L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
+.
+
+interpretation "parallel substritution" 'PSubst L T1 d e T2 = (ps L T1 d e T2).
+
+(* Basic properties *********************************************************)
+
+lemma subst_refl: ∀T,L,d,e. L ⊢ T [d, e] ≫ T.
+#T elim T -T //
+#I elim I -I /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
+                        ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+                        ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & 
+                                 L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 &
+                                 U2 =  𝕓{I} V2. T2.
+#d #e #L #U1 #U2 #H elim H -H d e L U1 U2
+[ #L #k #d #e #I #V1 #T1 #H destruct
+| #L #i #d #e #I #V1 #T1 #H destruct
+| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/
+| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct
+]
+qed.
+
+lemma subst_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫ U2 →
+                       ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & 
+                                L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 &
+                                U2 =  𝕓{I} V2. T2.
+/2/ qed.
+
+lemma subst_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
+                           ∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
+                           ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 &
+                                    U2 =  𝕗{I} V2. T2.
+#d #e #L #U1 #U2 #H elim H -H d e L U1 U2
+[ #L #k #d #e #I #V1 #T1 #H destruct
+| #L #i #d #e #I #V1 #T1 #H destruct
+| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/
+]
+qed.
+
+lemma subst_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫ U2 →
+                       ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 &
+                                U2 =  𝕗{I} V2. T2.
+/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/subst_defs.ma b/matita/matita/lib/lambda-delta/substitution/subst_defs.ma
deleted file mode 100644
index c563157f4..000000000
--- a/matita/matita/lib/lambda-delta/substitution/subst_defs.ma
+++ /dev/null
@@ -1,112 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/substitution/drop_defs.ma".
-
-(* TELESCOPIC SUBSTITUTION **************************************************)
-
-inductive subst: lenv → term → nat → nat → term → Prop ≝
-| subst_sort   : ∀L,k,d,e. subst L (⋆k) d e (⋆k)
-| subst_lref_lt: ∀L,i,d,e. i < d → subst L (#i) d e (#i)
-| subst_lref_be: ∀L,K,V,U1,U2,i,d,e.
-                 d ≤ i → i < d + e →
-                 ↑[0, i] K. 𝕓{Abbr} V ≡ L → subst K V 0 (d + e - i - 1) U1 →
-                 ↑[0, d] U1 ≡ U2 → subst L (#i) d e U2
-| subst_lref_ge: ∀L,i,d,e. d + e ≤ i → subst L (#i) d e (#(i - e))
-| subst_bind   : ∀L,I,V1,V2,T1,T2,d,e.
-                 subst L V1 d e V2 → subst (L. 𝕓{I} V1) T1 (d + 1) e T2 →
-                 subst L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
-| subst_flat   : ∀L,I,V1,V2,T1,T2,d,e.
-                 subst L V1 d e V2 → subst L T1 d e T2 →
-                 subst L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
-.
-
-interpretation "telescopic substritution" 'RSubst L T1 d e T2 = (subst L T1 d e T2).
-
-(* The basic properties *****************************************************)
-
-lemma subst_lift_inv: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀L. L ⊢ ↓[d,e] T2 ≡ T1.
-#d #e #T1 #T2 #H elim H -H d e T1 T2 /2/
-#i #d #e #Hdi #L >(minus_plus_m_m i e) in ⊢ (? ? ? ? ? %) /3/
-qed.
-(*
-| subst_lref_O : ∀L,V1,V2,e. subst L V1 0 e V2 →
-                 subst (L. 𝕓{Abbr} V1) #0 0 (e + 1) V2
-| subst_lref_S : ∀L,I,V,i,T1,T2,d,e.
-                 d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T2 ≡ T1 →
-                 subst (L. 𝕓{I} V) #(i + 1) (d + 1) e T2
-*)
-(* The basic inversion lemmas ***********************************************)
-
-lemma subst_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ ↓[d, e] U1 ≡ U2 →
-                           ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
-                           ∃∃V2,T2. subst L V1 d e V2 & 
-                                    subst (L. 𝕓{I} V1) T1 (d + 1) e T2 &
-                                    U2 =  𝕓{I} V2. T2.
-#d #e #L #U1 #U2 #H elim H -H d e L U1 U2
-[ #L #k #d #e #I #V1 #T1 #H destruct
-| #L #i #d #e #_ #I #V1 #T1 #H destruct
-| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
-| #L #i #d #e #_ #I #V1 #T1 #H destruct
-| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/
-| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct
-]
-qed.
-
-lemma subst_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ↓[d, e] 𝕓{I} V1. T1 ≡ U2 →
-                       ∃∃V2,T2. subst L V1 d e V2 & 
-                                subst (L. 𝕓{I} V1) T1 (d + 1) e T2 &
-                                U2 =  𝕓{I} V2. T2.
-/2/ qed.
-
-lemma subst_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ ↓[d, e] U1 ≡ U2 →
-                           ∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
-                           ∃∃V2,T2. subst L V1 d e V2 & subst L T1 d e T2 &
-                                    U2 =  𝕗{I} V2. T2.
-#d #e #L #U1 #U2 #H elim H -H d e L U1 U2
-[ #L #k #d #e #I #V1 #T1 #H destruct
-| #L #i #d #e #_ #I #V1 #T1 #H destruct
-| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
-| #L #i #d #e #_ #I #V1 #T1 #H destruct
-| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct
-| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/
-]
-qed.
-
-lemma subst_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ↓[d, e] 𝕗{I} V1. T1 ≡ U2 →
-                       ∃∃V2,T2. subst L V1 d e V2 & subst L T1 d e T2 &
-                                U2 =  𝕗{I} V2. T2.
-/2/ qed.
-(*
-lemma subst_inv_lref1_be_aux: ∀d,e,L,T,U. L ⊢ ↓[d, e] T ≡ U →
-                              ∀i. d ≤ i → i < d + e → T = #i →
-                              ∃∃K,V. ↑[0, i] K. 𝕓{Abbr} V ≡ L &
-                                     K ⊢ ↓[d, d + e - i - 1] V ≡ U.
-#d #e #L #T #U #H elim H -H d e L T U
-[ #L #k #d #e #i #_ #_ #H destruct
-| #L #j #d #e #Hid #i #Hdi #_ #H destruct -j;
-  lapply (le_to_lt_to_lt … Hdi … Hid) -Hdi Hid #Hdd
-  elim (lt_false … Hdd)
-| #L #K #V #U #j #d #e #_ #_ #HLK #HVU #_ #i #Hdi #Hide #H destruct -j /2/
-| #L #j #d #e #Hdei #i #_ #Hide #H destruct -j;
-  lapply (le_to_lt_to_lt … Hdei … Hide) -Hdei Hide #Hdede
-  elim (lt_false … Hdede)
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #_ #_ #H destruct
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #_ #_ #H destruct
-]
-qed.
-
-lemma subst_inv_lref1_be: ∀d,e,i,L,U. L ⊢ ↓[d, e] #i ≡ U →
-                          d ≤ i → i < d + e →
-                          ∃∃K,V. ↑[0, i] K. 𝕓{Abbr} V ≡ L &
-                                 K ⊢ ↓[d, d + e - i - 1] V ≡ U.
-/2/ qed.
-*)
diff --git a/matita/matita/lib/lambda-delta/substitution/thin_defs.ma b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
deleted file mode 100644
index c8ef44925..000000000
--- a/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
+++ /dev/null
@@ -1,44 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic
-    ||A||  Library of Mathematics, developed at the Computer Science
-    ||T||  Department of the University of Bologna, Italy.
-    ||I||
-    ||T||
-    ||A||  This file is distributed under the terms of the
-    \   /  GNU General Public License Version 2
-     \ /
-      V_______________________________________________________________ *)
-
-include "lambda-delta/substitution/subst_defs.ma".
-
-(* THINNING *****************************************************************)
-
-inductive thin: lenv → nat → nat → lenv → Prop ≝
-| thin_refl: ∀L. thin L 0 0 L
-| thin_thin: ∀L1,L2,I,V,e. thin L1 0 e L2 → thin (L1. 𝕓{I} V) 0 (e + 1) L2
-| thin_skip: ∀L1,L2,I,V1,V2,d,e.
-             thin L1 d e L2 → L1 ⊢ ↓[d,e] V1 ≡ V2 →
-             thin (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2)
-.
-
-interpretation "thinning" 'RSubst L1 d e L2 = (thin L1 d e L2).
-
-(* the basic inversion lemmas ***********************************************)
-
-lemma thin_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
-                          ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
-                          ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 &
-                                   K1 ⊢ ↓[d - 1, e] V1 ≡ V2 & 
-                                   L1 = K1. 𝕓{I} V1.
-#d #e #L1 #L2 #H elim H -H d e L1 L2
-[ #L #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V #e #_ #_ #H elim (lt_refl_false … H)
-| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #_ #I #L2 #V2 #H destruct -X Y Z;
-  /2 width=5/
-]
-qed.
-
-lemma thin_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d →
-                      ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & K1 ⊢ ↓[d - 1, e] V1 ≡ V2 &
-                               L1 = K1. 𝕓{I} V1.
-/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/thin_main.ma b/matita/matita/lib/lambda-delta/substitution/thin_main.ma
deleted file mode 100644
index f16fb3a48..000000000
--- a/matita/matita/lib/lambda-delta/substitution/thin_main.ma
+++ /dev/null
@@ -1,34 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "lambda-delta/substitution/thin_defs.ma".
-
-(* THINNING *****************************************************************)
-
-(* the main properties ******************************************************)
-
-axiom thin_conf_ge: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 →
-                    ∀e2,L2. ↓[0,e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0,e2-e1] L1 ≡ L2.
-
-axiom thin_conf_lt: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 →
-                    ∀e2,K2,I,V2. ↓[0,e2] L ≡ K2. 𝕓{I} V2 →
-                    e2 < d1 → let d ≝ d1 - e2 - 1 in
-                    ∃∃K1,V1. ↓[0,e2] L1 ≡ K1. 𝕓{I} V1 & ↓[d,e1] K2 ≡ K1 & ↑[d,e1] V1 ≡ V2.
-
-axiom thin_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
-                     ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 →
-                     ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2.
-
-axiom thin_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
-                     ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2.
diff --git a/matita/matita/lib/lambda-delta/syntax/item.ma b/matita/matita/lib/lambda-delta/syntax/item.ma
index 742ff2272..ea7a45362 100644
--- a/matita/matita/lib/lambda-delta/syntax/item.ma
+++ b/matita/matita/lib/lambda-delta/syntax/item.ma
@@ -16,6 +16,7 @@
  *)
 
 include "lambda-delta/ground.ma".
+include "lambda-delta/notation.ma".
 
 (* BINARY ITEMS *************************************************************)
 
diff --git a/matita/matita/lib/lambda-delta/xoa_defs.ma b/matita/matita/lib/lambda-delta/xoa_defs.ma
index 38c434304..5e66ef789 100644
--- a/matita/matita/lib/lambda-delta/xoa_defs.ma
+++ b/matita/matita/lib/lambda-delta/xoa_defs.ma
@@ -40,18 +40,11 @@ inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝
 
 interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
 
-inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝
-   | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ?
+inductive or3 (P0,P1,P2:Prop) : Prop ≝
+   | or3_intro0: P0 → or3 ? ? ?
+   | or3_intro1: P1 → or3 ? ? ?
+   | or3_intro2: P2 → or3 ? ? ?
 .
 
-interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3).
-
-inductive or4 (P0,P1,P2,P3:Prop) : Prop ≝
-   | or4_intro0: P0 → or4 ? ? ? ?
-   | or4_intro1: P1 → or4 ? ? ? ?
-   | or4_intro2: P2 → or4 ? ? ? ?
-   | or4_intro3: P3 → or4 ? ? ? ?
-.
-
-interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3).
+interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
 
diff --git a/matita/matita/lib/lambda-delta/xoa_notation.ma b/matita/matita/lib/lambda-delta/xoa_notation.ma
index 2e441f1cb..f21488be3 100644
--- a/matita/matita/lib/lambda-delta/xoa_notation.ma
+++ b/matita/matita/lib/lambda-delta/xoa_notation.ma
@@ -30,11 +30,7 @@ notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break &
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0},${ident x1},${ident x2}.$P0) (λ${ident x0},${ident x1},${ident x2}.$P1) (λ${ident x0},${ident x1},${ident x2}.$P2) }.
 
-notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+notation "hvbox(∨∨ term 19 P0 break | term 19 P1 break | term 19 P2)"
  non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1},${ident x2}.$P0) (λ${ident x0},${ident x1},${ident x2}.$P1) (λ${ident x0},${ident x1},${ident x2}.$P2) (λ${ident x0},${ident x1},${ident x2}.$P3) }.
-
-notation "hvbox(∨∨ term 19 P0 break | term 19 P1 break | term 19 P2 break | term 19 P3)"
- non associative with precedence 20
- for @{ 'Or $P0 $P1 $P2 $P3 }.
+ for @{ 'Or $P0 $P1 $P2 }.