- first properties of strongly normalizing terms

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / computation / lsubc_ldrop.ma

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 fcc7f683d2184ac8785e32484f5f20d28ebfa922..03ea7b6289922c57c645eee94c05369545162883 100644 (file)
--- 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/
   ]
 ]