X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Facp_aaa.ma;h=2ffff40df125eb499b27660dafbae2881ac784d0;hb=fba384e357ed3c8781fc018c2c16f2b40df144af;hp=f4da11310f6e055a168f11605d84f7a1701344bb;hpb=38c81062ae1aedf89d426d5dcd9a27824c4b0fb0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
index f4da11310..2ffff40df 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
@@ -31,7 +31,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
 #RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
 [ #L #k #L0 #des #HL0 #X #H #L2 #HL20
   >(lifts_inv_sort1 … H) -H
-  lapply (aacr_acr … H1RP H2RP ⓪) #HAtom
+  lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom
   @(s2 … HAtom … ◊) // /2 width=2/
 | #I #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
   lapply (aacr_acr … H1RP H2RP B) #HB