We reintroduce the distinction between binding and non-binding items.

Mon-binding items are now forbidden in environments

diff --git a/matita/matita/lib/lambda-delta/language/item.ma b/matita/matita/lib/lambda-delta/language/item.ma
index d85127ad7645537ccf708a501e986cffa0a3a28d..60a115dc0947968a212e51d7df6a8c902d8367f7 100644 (file)
--- a/matita/matita/lib/lambda-delta/language/item.ma
+++ b/matita/matita/lib/lambda-delta/language/item.ma
@@ -19,22 +19,41 @@ include "lambda-delta/ground.ma".
 
 (* BINARY ITEMS *************************************************************)
 
+(* binary binding items *)
+inductive bind2: Type[0] ≝
+| Abbr: bind2 (* abbreviation *)
+| Abst: bind2 (* abstraction *)
+.
+
+(* binary non-binding items *)
+inductive flat2: Type[0] ≝
+| Appl: flat2 (* application *)
+| Cast: flat2 (* explicit type annotation *)
+.
+
 (* binary items *)
 inductive item2: Type[0] ≝
-   | Abbr: item2 (* abbreviation *)
-   | Abst: item2 (* abstraction *)
-   | Appl: item2 (* application *)
-   | Cast: item2 (* explicit type annotation *)
+| Bind: bind2 → item2 (* binding item *)
+| Flat: flat2 → item2 (* non-binding item *)
 .
 
+coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2.
+
+coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2.
+
 (* reduction-related categorization *****************************************)
 
-(* binary items entitled for zeta-reduction *)
-definition zable2 ≝ λI. I = Abbr ∨ I = Cast.
+(* binding items entitled for zeta-reduction *)
+definition zable ≝ λI. I = Abbr.
+
+interpretation "is entitled for zeta-reduction" 'Zeta I = (zable I).
+
+(* non-binding items entitled for zeta-reduction *)
+definition table ≝ λI. I = Cast.
 
-interpretation "is entitled for zeta-reduction" 'Zeta I = (zable2 I).
+interpretation "is entitled for tau-reduction" 'Tau I = (table I).
 
-(* binary items entitled for theta reduction *)
-definition thable2 ≝ λI. I = Abbr.
+(* binding items entitled for theta-reduction *)
+definition thable ≝ λI. I = Abbr.
 
-interpretation "is entitled for theta-reduction" 'Theta I = (thable2 I).
+interpretation "is entitled for theta-reduction" 'Theta I = (thable I).

diff --git a/matita/matita/lib/lambda-delta/language/lenv.ma b/matita/matita/lib/lambda-delta/language/lenv.ma
index 018b3b4ffeb0174bc5e97cb20a3387216096441d..3398de4eeb4b6d3caa7ae541e1d42b3f98ae1861 100644 (file)
--- a/matita/matita/lib/lambda-delta/language/lenv.ma
+++ b/matita/matita/lib/lambda-delta/language/lenv.ma
@@ -15,10 +15,10 @@ include "lambda-delta/language/term.ma".
 
 (* local environments *)
 inductive lenv: Type[0] ≝
-   | LSort: lenv                       (* empty *)
-   | LCon2: lenv → item2 → term → lenv (* binary item construction *)
+| LSort: lenv                       (* empty *)
+| LPair: lenv → bind2 → term → lenv (* binary binding construction *)
 .
 
 interpretation "sort (local environment)" 'Star = LSort.
 
-interpretation "environment construction (binary)" 'DCon L I T = (LCon2 L I T).
+interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T).

diff --git a/matita/matita/lib/lambda-delta/language/term.ma b/matita/matita/lib/lambda-delta/language/term.ma
index 22dad92a5855b50a4e284714124f4f4391bacff1..ac3b8fa5e6df803e7d912e9cec8d560ddb74d043 100644 (file)
--- a/matita/matita/lib/lambda-delta/language/term.ma
+++ b/matita/matita/lib/lambda-delta/language/term.ma
@@ -15,13 +15,17 @@ include "lambda-delta/language/item.ma".
 
 (* terms *)
 inductive term: Type[0] ≝
-   | TSort: nat → term                 (* sort: starting at 0 *)
-   | TLRef: nat → term                 (* reference by index: starting at 0 *)
-   | TCon2: item2 → term → term → term (* binary construction *)
+| TSort: nat → term                 (* sort: starting at 0 *)
+| TLRef: nat → term                 (* reference by index: starting at 0 *)
+| TPair: item2 → term → term → term (* binary item construction *)
 .
 
 interpretation "sort (term)" 'Star k = (TSort k).
 
 interpretation "local reference (term)" 'Weight i = (TLRef i).
 
-interpretation "term construction (binary)" 'SCon I T1 T2 = (TCon2 I T1 T2).
+interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).
+
+interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2).
+
+interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2).

diff --git a/matita/matita/lib/lambda-delta/language/weight.ma b/matita/matita/lib/lambda-delta/language/weight.ma
index f6be4dab7d45b2897afe7bfe73a68f1ea1f526fe..f0021be9e278c4cf59ee085e9167a425222c2dd1 100644 (file)
--- a/matita/matita/lib/lambda-delta/language/weight.ma
+++ b/matita/matita/lib/lambda-delta/language/weight.ma
@@ -15,18 +15,18 @@ include "lambda-delta/language/lenv.ma".
 
 (* the weight of a term *)
 let rec tw T ≝ match T with
-   [ TSort _     ⇒ 1
-   | TLRef _     ⇒ 1
-   | TCon2 _ V T ⇒ tw V + tw T + 1
-   ].
+[ TSort _     ⇒ 1
+| TLRef _     ⇒ 1
+| TPair _ V T ⇒ tw V + tw T + 1
+].
 
 interpretation "weight (term)" 'Weight T = (tw T).
 
 (* the weight of a local environment *)
 let rec lw L ≝ match L with
-   [ LSort       ⇒ 0
-   | LCon2 L _ V ⇒ lw L + #V
-   ].
+[ LSort       ⇒ 0
+| LPair L _ V ⇒ lw L + #V
+].
 
 interpretation "weight (local environment)" 'Weight L = (lw L).
 

diff --git a/matita/matita/lib/lambda-delta/notation.ma b/matita/matita/lib/lambda-delta/notation.ma
index 0f6387e03c42dd100ae6c32aa41e9413cf34f69d..7f5fabf28821582db43d4a35fc376bcd553d46a8 100644 (file)
--- a/matita/matita/lib/lambda-delta/notation.ma
+++ b/matita/matita/lib/lambda-delta/notation.ma
@@ -17,6 +17,10 @@ notation "hvbox( ζ I )"
  non associative with precedence 45
  for @{ 'Zeta $I }.
 
+notation "hvbox( τ I )"
+ non associative with precedence 45
+ for @{ 'Tau $I }.
+
 notation "hvbox( θ I )"
  non associative with precedence 45
  for @{ 'Theta $I }.
@@ -29,13 +33,21 @@ notation "hvbox( ⋆ k )"
  non associative with precedence 90
  for @{ 'Star $k }.
 
-notation "hvbox( ♭ (term 90 I) break (term 90 T1) . break (term 90 T) )"
+notation "hvbox( 𝕚 { I } break (term 90 T1) . break (term 90 T) )"
+ non associative with precedence 90
+ for @{ 'SItem $I $T1 $T }.
+
+notation "hvbox( 𝕓 { I } break (term 90 T1) . break (term 90 T) )"
+ non associative with precedence 90
+ for @{ 'SBind $I $T1 $T }.
+
+notation "hvbox( 𝕗 { I } break (term 90 T1) . break (term 90 T) )"
  non associative with precedence 90
- for @{ 'SCon $I $T1 $T }.
+ for @{ 'SFlat $I $T1 $T }.
 
-notation "hvbox( T . break ♭ (term 90 I) break (term 90 T1) )"
+notation "hvbox( T . break 𝕓 { I } break (term 90 T1) )"
  non associative with precedence 89
- for @{ 'DCon $T $I $T1 }.
+ for @{ 'DBind $T $I $T1 }.
 
 notation "hvbox( # term 90 x )"
  non associative with precedence 90

diff --git a/matita/matita/lib/lambda-delta/substitution/lift.ma b/matita/matita/lib/lambda-delta/substitution/lift.ma
index 9067889686fa20b2552600edb32e3de17ffd228a..6569461718d2e46e81c9f40cd1d34e260203ba5f 100644 (file)
--- a/matita/matita/lib/lambda-delta/substitution/lift.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift.ma
@@ -14,12 +14,15 @@ include "lambda-delta/language/term.ma".
 (* RELOCATION ***************************************************************)
 
 inductive lift: term → nat → nat → term → Prop ≝
-   | lift_sort   : ∀k,d,e. lift (⋆k) d e (⋆k)
-   | lift_lref_lt: ∀i,d,e. i < d → lift (#i) d e (#i)
-   | lift_lref_ge: ∀i,d,e. d ≤ i → lift (#i) d e (#(i + e))
-   | lift_con2   : ∀I,V1,V2,T1,T2,d,e.
-                   lift V1 d e V2 → lift T1 (d + 1) e T2 →
-                   lift (♭I V1. T1) d e (♭I V2. T2)
+| lift_sort   : ∀k,d,e. lift (⋆k) d e (⋆k)
+| lift_lref_lt: ∀i,d,e. i < d → lift (#i) d e (#i)
+| lift_lref_ge: ∀i,d,e. d ≤ i → lift (#i) d e (#(i + e))
+| lift_bind   : ∀I,V1,V2,T1,T2,d,e.
+                lift V1 d e V2 → lift T1 (d + 1) e T2 →
+                lift (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
+| lift_flat   : ∀I,V1,V2,T1,T2,d,e.
+                lift V1 d e V2 → lift T1 d e T2 →
+                lift (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
 .
 
 interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2).
@@ -34,9 +37,10 @@ qed.
 
 lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
 #d #e #T1 #T2 #H elim H -H d e T1 T2 //
-   [ #i #d #e #_ #k #H destruct
-   | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
-   ]
+[ #i #d #e #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
+]
 qed.
 
 lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k.
@@ -46,11 +50,12 @@ qed.
 lemma lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i →
                           (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
 #d #e #T1 #T2 #H elim H -H d e T1 T2
-   [ #k #d #e #i #H destruct
-   | #j #d #e #Hj #i #Hi destruct /3/
-   | #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4/
-   | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
-   ]
+[ #k #d #e #i #H destruct
+| #j #d #e #Hj #i #Hi destruct /3/
+| #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4/
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+]
 qed.
 
 lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
@@ -58,23 +63,42 @@ lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
 #d #e #T1 #i #H lapply (lift_inv_lref2_aux … H) /2/
 qed.
 
-lemma lift_inv_con22_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
-                          ∀I,V2,U2. T2 = ♭I V2.U2 →
+lemma lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+                          ∀I,V2,U2. T2 = 𝕓{I} V2.U2 →
                           ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
-                                   T1 = ♭I V1.U1.
+                                   T1 = 𝕓{I} V1.U1.
 #d #e #T1 #T2 #H elim H -H d e T1 T2
-   [ #k #d #e #I #V2 #U2 #H destruct
-   | #i #d #e #_ #I #V2 #U2 #H destruct
-   | #i #d #e #_ #I #V2 #U2 #H destruct
-   | #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct
-     /2 width = 5/
-   ]
+[ #k #d #e #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /2 width = 5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct
+]
 qed.
 
-lemma lift_inv_con22: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  ♭I V2. U2 →
+lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  𝕓{I} V2. U2 →
                       ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
-                               T1 = ♭I V1. U1.
-#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_con22_aux … H) /2/
+                               T1 = 𝕓{I} V1. U1.
+#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_bind2_aux … H) /2/
+qed.
+
+lemma lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+                          ∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
+                          ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
+                                   T1 = 𝕗{I} V1.U1.
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+[ #k #d #e #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /2 width = 5/
+]
+qed.
+
+lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  𝕗{I} V2. U2 →
+                      ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
+                               T1 = 𝕗{I} V1. U1.
+#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_flat2_aux … H) /2/
 qed.
 
 (* the main properies *******************************************************)
@@ -84,42 +108,49 @@ theorem lift_trans_rev: ∀d1,e1,T1,T. ↑[d1,e1] T1 ≡ T →
                         d1 ≤ d2 →
                         ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1.
 #d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
-   [ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
-     lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct -T2 /3/
-   | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
-     lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2
-     [ -Hid2 /4/
-     | elim (lt_false d1 ?)
-       @(le_to_lt_to_lt … Hd12) -Hd12 @(le_to_lt_to_lt … Hid1) -Hid1 /2/
-     ]
-   | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
-     lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2
-     [ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/
-     | -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2
-       @(ex2_1_intro … #(i - e2))
-       [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ]
-       | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /3/
-       ]
-     ]
-   | #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
-     lapply (lift_inv_con22 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
-     elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
-     >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /3 width = 5/
-   ]
+[ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
+  lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct -T2 /3/
+| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
+  lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2
+  [ -Hid2 /4/
+  | elim (lt_false d1 ?)
+    @(le_to_lt_to_lt … Hd12) -Hd12 @(le_to_lt_to_lt … Hid1) -Hid1 /2/
+  ]
+| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
+  lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2
+  [ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/
+  | -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2
+    @(ex2_1_intro … #(i - e2))
+    [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ]
+    | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %) /3/
+    ]
+  ]
+| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
+  lapply (lift_inv_bind2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
+  elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
+  >plus_plus_comm_23 in HU2 #HU2 elim (IHU … HU2 ?) /3 width = 5/
+| #I #W1 #W #U1 #U #d1 #e1 #_ #_ #IHW #IHU #d2 #e2 #T2 #H #Hd12
+  lapply (lift_inv_flat2 … H) -H * #W2 #U2 #HW2 #HU2 #H destruct -T2;
+  elim (IHW … HW2 ?) // -IHW HW2 #W0 #HW2 #HW1
+  elim (IHU … HU2 ?) /3 width = 5/
+]
 qed.
 
 theorem lift_free: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1.
                                  d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 →
                                  ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2.
 #d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2
-   [ /3/
-   | #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
-     lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/
-   | #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
-     lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21
-     <(plus_plus_minus_m_m e1 e2 i) /3/
-   | #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
-     elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b 
-     elim (IHT (d2+1) … ? ? He12) /3 width = 5/
-   ]
+[ /3/
+| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
+  lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/
+| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
+  lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21
+  <(plus_plus_minus_m_m e1 e2 i) /3/
+| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
+  elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
+  elim (IHT (d2+1) … ? ? He12) /3 width = 5/
+| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
+  elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
+  elim (IHT d2 … ? ? He12) /3 width = 5/
+]
 qed.

diff --git a/matita/matita/lib/lambda-delta/substitution/subst.ma b/matita/matita/lib/lambda-delta/substitution/subst.ma
index 519aeaa19ce6c5f657e51bfa432d08ac75175539..5989693c5059a987e6e77a8a0c0b0fee9d4c8d71 100644 (file)
--- a/matita/matita/lib/lambda-delta/substitution/subst.ma
+++ b/matita/matita/lib/lambda-delta/substitution/subst.ma
@@ -15,16 +15,19 @@ include "lambda-delta/substitution/lift.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_O : ∀L,V,e. 0 < e → subst (L. ♭Abbr V) #0 0 e V
-   | subst_lref_S : ∀L,I,V,i,T1,T2,d,e. 
-                    d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T1 ≡ T2 →
-                    subst (L. ♭I V) #(i + 1) (d + 1) e T2
-   | subst_lref_ge: ∀L,i,d,e. d + e ≤ i → subst L (#i) d e (#(i - e))
-   | subst_con2   : ∀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_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_O : ∀L,V,e. 0 < e → subst (L. 𝕓{Abbr} V) #0 0 e V
+| subst_lref_S : ∀L,I,V,i,T1,T2,d,e.
+                 d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T1 ≡ T2 →
+                 subst (L. 𝕓{I} V) #(i + 1) (d + 1) e T2
+| 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).

diff --git a/matita/matita/lib/lambda-delta/substitution/thin.ma b/matita/matita/lib/lambda-delta/substitution/thin.ma
index ab1c5f2717e472a25108c32dc7abc987c9fdd83c..96432922dc5d1dd29ededb2e0d2fdd912ed754cd 100644 (file)
--- a/matita/matita/lib/lambda-delta/substitution/thin.ma
+++ b/matita/matita/lib/lambda-delta/substitution/thin.ma
@@ -14,12 +14,11 @@ include "lambda-delta/substitution/subst.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)
+| 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).
@@ -30,6 +29,6 @@ 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,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.
+                    ∃∃K1,V1. ↓[0,e2] L1 ≡ K1. 𝕓{I} V1 & ↓[d,e1] K2 ≡ K1 & ↑[d,e1] V1 ≡ V2.