X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fldrop.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fldrop.ma;h=db31dfaab4d2bc0c827dc39c1631324497904adc;hb=48e1e9851375f52d26ccba5bf4babd0b3474d869;hp=ffd44c5aa7eaf808836f6d36fe5b2d0f4666c0fa;hpb=18ac3a120a3887b144c1d0e13d64d6e1c2d10d93;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
index ffd44c5aa..db31dfaab 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
@@ -16,7 +16,7 @@ include "Basic_2/grammar/lenv_weight.ma".
 include "Basic_2/grammar/lsubs.ma".
 include "Basic_2/substitution/lift.ma".
 
-(* DROPPING *****************************************************************)
+(* LOCAL ENVIRONMENT SLICING ************************************************)
 
 (* Basic_1: includes: ldrop_skip_bind *)
 inductive ldrop: nat → nat → relation lenv ≝
@@ -33,7 +33,7 @@ interpretation "ldropping" 'RDrop d e L1 L2 = (ldrop d e L1 L2).
 (* Basic inversion lemmas ***************************************************)
 
 fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2.
-#d #e #L1 #L2 * -d e L1 L2
+#d #e #L1 #L2 * -d -e -L1 -L2
 [ //
 | //
 | #L1 #L2 #I #V #e #_ #_ #H
@@ -49,7 +49,7 @@ lemma ldrop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2.
 
 fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ →
                           L2 = ⋆.
-#d #e #L1 #L2 * -d e L1 L2
+#d #e #L1 #L2 * -d -e -L1 -L2
 [ //
 | #L #I #V #H destruct
 | #L1 #L2 #I #V #e #_ #H destruct
@@ -65,10 +65,10 @@ fact ldrop_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] K ≡ L2).
-#d #e #L1 #L2 * -d e L1 L2
+#d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #K #I #V #H destruct
-| #L #I #V #_ #K #J #W #HX destruct -L I V /3/
-| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct -L1 I V /3/
+| #L #I #V #_ #K #J #W #HX destruct /3 width=1/
+| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1/
 | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H)
 ]
 qed.
@@ -76,13 +76,13 @@ qed.
 lemma ldrop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 →
                     (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
                     (0 < e ∧ ↓[0, e - 1] K ≡ L2).
-/2/ qed-.
+/2 width=3/ qed-.
 
 (* Basic_1: was: ldrop_gen_ldrop *)
 lemma ldrop_inv_ldrop1: ∀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 (ldrop_inv_O1 … H) -H * // #H destruct -e;
+elim (ldrop_inv_O1 … H) -H * // #H destruct
 elim (lt_refl_false … He)
 qed-.
 
@@ -91,12 +91,11 @@ fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
                           ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 &
                                    ↑[d - 1, e] V2 ≡ V1 & 
                                    L2 = K2. 𝕓{I} V2.
-#d #e #L1 #L2 * -d e L1 L2
+#d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #I #K #V #H destruct
 | #L #I #V #H elim (lt_refl_false … H)
 | #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H)
-| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct -X Y Z
-  /2 width=5/
+| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct /2 width=5/
 ]
 qed.
 
@@ -105,19 +104,18 @@ lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ↓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0
                        ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 &
                                 ↑[d - 1, e] V2 ≡ V1 & 
                                 L2 = K2. 𝕓{I} V2.
-/2/ qed-.
+/2 width=3/ qed-.
 
 fact ldrop_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 &
                                    ↑[d - 1, e] V2 ≡ V1 & 
                                    L1 = K1. 𝕓{I} V1.
-#d #e #L1 #L2 * -d e L1 L2
+#d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #I #K #V #H destruct
 | #L #I #V #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/
+| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct /2 width=5/
 ]
 qed.
 
@@ -125,7 +123,7 @@ qed.
 lemma ldrop_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-.
+/2 width=3/ qed-.
 
 (* Basic properties *********************************************************)
 
@@ -136,7 +134,7 @@ qed.
 
 lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e.
                       ↓[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/
+#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
 lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
@@ -144,27 +142,27 @@ lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
                                d ≤ i → i < d + e →
                                ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 &
                                      ↓[0, i] L2 ≡ K2. 𝕓{Abbr} V.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
 [ #d #e #K1 #V #i #H
   lapply (ldrop_inv_atom1 … H) -H #H destruct
 | #L1 #L2 #K1 #V #i #_ #_ #H
   elim (lt_zero_false … H)
 | #L1 #L2 #V #e #HL12 #IHL12 #K1 #W #i #H #_ #Hie
   elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
-  [ -IHL12 Hie; destruct -i K1 W;
-    <minus_n_O <minus_plus_m_m /2/
-  | -HL12;
-    elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/
+  [ -IHL12 -Hie destruct
+    <minus_n_O <minus_plus_m_m // /2 width=3/
+  | -HL12
+    elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/
   ]
 | #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie
   elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
-  [ -IHL12 Hie Hi; destruct
-  | elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/
+  [ -IHL12 -Hie -Hi destruct
+  | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/
   ]
 | #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
   lapply (plus_S_le_to_pos … Hdi) #Hi
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1
-  elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 [2: /2/ |3: /2/ ] -Hdi Hide >arith_g1 // /3/
+  elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 /2 width=1/ -Hdi -Hide >arith_g1 // /3 width=3/
 ]
 qed.
 
@@ -177,17 +175,17 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 →
 [ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct
 | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
   elim (ldrop_inv_O1 … H) -H * #He #H
-  [ -IHL1; destruct -e K2 I2 V2 /2/
-  | @ldrop_ldrop >(plus_minus_m_m e 1) /2/
+  [ -IHL1 destruct /2 width=1/
+  | @ldrop_ldrop >(plus_minus_m_m e 1) // /2 width=3/
   ]
 ]
 qed-.
 
 lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1].
-#L1 #L2 #d #e #H elim H -H L1 L2 d e // normalize
-[ /2/
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
+[ /2 width=1/
 | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
-  >(tw_lift … HV21) -HV21 /2/
+  >(tw_lift … HV21) -HV21 /2 width=1/
 ]
 qed-. 
 
@@ -197,8 +195,8 @@ lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e.
 [ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct
 | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
   elim (ldrop_inv_O1 … H) -H * #He #H
-  [ -IHL1; destruct -e K2 I2 V2 //
-  | lapply (IHL1 … H) -IHL1 H #HeK1 whd in ⊢ (? ? %) /2/
+  [ -IHL1 destruct //
+  | lapply (IHL1 … H) -IHL1 -H #HeK1 whd in ⊢ (? ? %); /2 width=1/
   ]
 ]
 qed-.
@@ -208,8 +206,8 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e.
 [ #L2 #e #H >(ldrop_inv_atom1 … H) -H //
 | #K1 #I1 #V1 #IHL1 #L2 #e #H
   elim (ldrop_inv_O1 … H) -H * #He #H
-  [ -IHL1; destruct -e L2 //
-  | lapply (IHL1 … H) -IHL1 H #H >H -H; normalize
+  [ -IHL1 destruct //
+  | lapply (IHL1 … H) -IHL1 -H #H >H -H normalize
     >minus_le_minus_minus_comm //
   ]
 ]