X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fldrop_append.ma;h=a122f9d452c4fda173f0b878e606b70208067a28;hb=c841fac6721efd9ec54ba1ce8479c43ff2389b91;hp=359d39c80c4ea0a59c82a9809a79504730cb1a29;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma
index 359d39c80..a122f9d45 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma
@@ -18,7 +18,7 @@ include "basic_2/substitution/ldrop.ma".
 
 (* Properties on append for local environments ******************************)
 
-fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → 
+fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
                                 d = 0 → e ≤ |L1| →
                                 ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // /4 width=1/
@@ -54,9 +54,11 @@ lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e ≤
   [ #H1 #_ #K2 #H2
     lapply (ldrop_inv_refl … H1) -H1 #H1
     lapply (ldrop_inv_refl … H2) -H2 #H2 destruct //
-  | #e #_ #H1 #H1e #K2 #H2
+  | #e #_ #H1 #H #K2 #H2
+    lapply (le_plus_to_le_r … H) -H
     lapply (ldrop_inv_ldrop1 … H1 ?) -H1 //
-    lapply (ldrop_inv_ldrop1 … H2 ?) -H2 // /3 width=4/
+    lapply (ldrop_inv_ldrop1 … H2 ?) -H2 //
+    <minus_plus_m_m /2 width=4/
   ]
 ]
-qed-. 
+qed-.