X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fcpy_nlift.ma;h=5f1148dbf260d46656bce852484cad6cee7931ad;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=226f6afab9adbe761315e2d75f9da140d9044852;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma
index 226f6afab..5f1148dbf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_nlift.ma
@@ -47,7 +47,7 @@ lemma cpy_fwd_nlift2_ge: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 →
     | * #J #K #W #j #Hdj #Hji #HLK #HnW
       elim (yle_inv_succ1 … Hdj) -Hdj #Hdj #Hj
       lapply (ylt_O … Hj) -Hj #Hj
-      lapply (ldrop_inv_drop1_lt … HLK ?) // -HLK #HLK
+      lapply (drop_inv_drop1_lt … HLK ?) // -HLK #HLK
       >(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ]
       #HnU1 <minus_le_minus_minus_comm in HnW;
       /5 width=9 by nlift_bind_dx, monotonic_lt_pred, lt_plus_to_minus_r, ex5_4_intro, or_intror/