- ldrop is now drop as in basic_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cnr_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
index 83def4723d6662825db52d02fa89e621807c6a0b..001f2017f5fdff5528aa0e9836589c288d0bc662 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
@@ -24,7 +24,7 @@ lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ ➡ 
 #G #L #K #V #i #HLK #X #H
 elim (cpr_inv_lref1 … H) -H // *
 #K0 #V1 #V2 #HLK0 #_ #_
-lapply (ldrop_mono … HLK … HLK0) -L #H destruct
+lapply (drop_mono … HLK … HLK0) -L #H destruct
 qed.
 
 (* Relocation properties ****************************************************)