commit by user lroversi

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / ldrop_append.ma

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 359d39c80c4ea0a59c82a9809a79504730cb1a29..a122f9d452c4fda173f0b878e606b70208067a28 100644 (file)
--- 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-.