X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Fgcp_aaa.ma;h=40e757ad62b4c9bd4445c6e82a1cfd5b492ace06;hp=750c3a538c19a2c41b938ac5af2ae8e4b84bfcb2;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
index 750c3a538..40e757ad6 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
@@ -37,7 +37,7 @@ theorem acr_aaa_lsubc_lifts (RR) (RS) (RP):
   elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
   lapply (acr_gcr … H1RP H2RP A) #HA
   lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H
-  elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
+  elim (drops_split_trans … H) -H [ |*: /2 width=6 by pr_after_nat_uni/ ] #Y #HLK0 #HY
   lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
   elim (drops_inv_skip2 … HY) -HY #Z #K0 #HK01 #HZ #H destruct
   elim (liftsb_inv_pair_sn … HZ) -HZ #V0 #HV10 #H destruct