X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Flpx_aaa.ma;h=3537c8d01af5e424142f2d4f4e303ef499d3582a;hb=e5378812c068074f0ac627541d3f066e135c8824;hp=e21810ea582ec56adb09cc452c207c4a37982768;hpb=928cfe1ebf2fbd31731c8851cdec70802596016d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
index e21810ea5..3537c8d01 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
@@ -36,7 +36,7 @@ lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
     lapply (ldrop_mono … H … HLK1) -H #H destruct
     elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
     elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
-    lapply (ldrop_fwd_ldrop2 … HLK2) -V0 /3 width=7/
+    lapply (ldrop_fwd_drop2 … HLK2) -V0 /3 width=7/
   ]
 | #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
   elim (cpx_inv_abbr1 … H) -H *