xoa: change in naming convenctions for existential quantifies

[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..38244e6be64891519c1879c9bbb09c8ba81dc806 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma
@@ -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-.