X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fcnx.ma;h=2402ccf0bd5f0740bbf5aebeca1922d610559daa;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=a464e95befd04d813146a6711cf0a325911ea804;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
index a464e95be..2402ccf0b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
@@ -108,12 +108,12 @@ qed.
 
 lemma cnx_lref_free: ∀h,g,G,L,i. |L| ≤ i → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄.
 #h #g #G #L #i #Hi #X #H elim (cpx_inv_lref1 … H) -H // *
-#I #K #V1 #V2 #HLK lapply (ldrop_fwd_length_lt2 … HLK) -HLK
+#I #K #V1 #V2 #HLK lapply (drop_fwd_length_lt2 … HLK) -HLK
 #H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
 qed.
 
 lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄.
-#h #g #G #L #i #HL @cnx_lref_free >(ldrop_fwd_length … HL) -HL //
+#h #g #G #L #i #HL @cnx_lref_free >(drop_fwd_length … HL) -HL //
 qed.
 
 lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →