X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Flsubc_ldrop.ma;h=03ea7b6289922c57c645eee94c05369545162883;hb=011cf6478141e69822a5b40933f2444d0522532f;hp=fcc7f683d2184ac8785e32484f5f20d28ebfa922;hpb=48b202cd4ccd3ffc10f9a134314f747fdee30d36;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma
index fcc7f683d..03ea7b628 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma
@@ -61,7 +61,7 @@ lemma ldrop_lsubc_trans: ∀RR,RS,RP.
   | #K2 #W2 #A #HV2 #HW2 #HK12 #H1 #H2 destruct
     elim (IHLK1 … HK12) #K #HL1K #HK2
     lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA
-    lapply (s7 … HA … HV2 HLK1 HV21) -HV2
+    lapply (s7 … HA … HV2 … HLK1 HV21) -HV2
     elim (lift_total W2 d e) /4 width=9/
   ]
 ]