X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Faaa_ssta.ma;h=5cccd8fe1d6ccf11bd265c44dcb9cc131324b6cf;hb=e5378812c068074f0ac627541d3f066e135c8824;hp=45cf9cda7a73dbe6c710e2a03347df77dcbc5bb5;hpb=928cfe1ebf2fbd31731c8851cdec70802596016d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma
index 45cf9cda7..5cccd8fe1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma
@@ -27,7 +27,7 @@ lemma aaa_ssta_conf: ∀h,g,G,L. Conf3 … (aaa G L) (ssta h g G L).
 | #I #G #L #K #V #B #i #HLK #HV #IHV #U #H
   elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HU
   lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H0 destruct
-  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
   @(aaa_lift … HLK … HU) -HU -L // -HV /2 width=2/
 | #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #H
   elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/