X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Ftps_tps.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Ftps_tps.ma;h=7cc9b2f9e7ed5774ae9988779f35d40d9defda93;hb=035e3f52f8da3cb3cdb493aa20568ad673cc2cf5;hp=d9e9e12f95e20def1e45a4ab3ea56cbd1e056740;hpb=83aea9a1662de32505512d6296921ebfffcfc53d;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_tps.ma
index d9e9e12f9..7cc9b2f9e 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_tps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_tps.ma
@@ -28,7 +28,7 @@ theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫ T1 →
   elim (tps_inv_lref1 … H) -H
   [ #HX destruct -T2 /4/
   | -Hd1 Hde1 * #K2 #V2 #_ #_ #HLK2 #HVT2
-    lapply (drop_mono … HLK1 … HLK2) -HLK1 HLK2 #H destruct -V1 K1
+    lapply (ldrop_mono … HLK1 … HLK2) -HLK1 HLK2 #H destruct -V1 K1
     >(lift_mono … HVT1 … HVT2) -HVT1 HVT2 /2/
   ]
 | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX