X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Fsta_aaa.ma;h=affd2ededc64f5af2e6ef8c3b9628b35d2067c9b;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=c49c6ee2101ea890de1820bcb98429e6628dbb20;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sta_aaa.ma
index c49c6ee21..affd2eded 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/sta_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/sta_aaa.ma
@@ -37,8 +37,8 @@ lemma sta_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (sta h G L).
   lapply (sta_inv_sort1 … H) -H #H destruct //
 | #I #G #L #K #V #B #i #HLK #HV #IHV #U #H
   elim (sta_inv_lref1 … H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HU
-  lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H0 destruct
-  lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
+  lapply (drop_mono … HLK0 … HLK) -HLK0 #H0 destruct
+  lapply (drop_fwd_drop2 … HLK) -HLK #HLK
   @(aaa_lift … HLK … HU) -HU -L /2 width=2 by/
 | #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #H
   elim (sta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2 by aaa_abbr/