X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Facp_aaa.ma;h=f4da11310f6e055a168f11605d84f7a1701344bb;hb=f7386d0b74f935f07ede4be46d0489a233d68b85;hp=1b2536c8b2b559a92cce195314fde89a0f14cc86;hpb=708aa01d44c67343f0dac0353b52c7c2457069b3;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma
index 1b2536c8b..f4da11310 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma
@@ -58,13 +58,13 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
     @(s4 … HB … ◊ … HV2 HLK2)
     @(s7 … HB … HKV2B) //
   ]
-| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
+| #a #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
   elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
   lapply (aacr_acr … H1RP H2RP A) #HA
   lapply (aacr_acr … H1RP H2RP B) #HB
   lapply (s1 … HB) -HB #HB
   @(s5 … HA … ◊ ◊) // /3 width=5/
-| #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
+| #a #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
   elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
   @(aacr_abst  … H1RP H2RP)
   [ lapply (aacr_acr … H1RP H2RP B) #HB