X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fcomputation%2Fgcp_aaa.ma;h=1cb4da56a12270f5cece20c831e20483fcec71cd;hb=291fe1d3b56faf91d07099f43f3ebde2988649e1;hp=3082b22de0a59177434fbb9ccc99a86ef0eb10b7;hpb=b5507c449ba38a76666a35664f9cf4e1953ad8ec;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/gcp_aaa.ma
index 3082b22de..1cb4da56a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/gcp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/gcp_aaa.ma
@@ -67,8 +67,8 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
   @(acr_abst  … H1RP H2RP) /2 width=5 by/
   #L3 #V3 #W3 #T3 #cs3 #HL32 #HW03 #HT03 #H1B #H2B
   elim (drops_lsubc_trans … H1RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
-  lapply (aaa_lifts … L2 W3 … (cs ;; cs3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
-  @(IHA (L2. ⓛW3) … (cs + 1 ;; cs3 + 1)) -IHA
+  lapply (aaa_lifts … L2 W3 … (cs ● cs3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
+  @(IHA (L2. ⓛW3) … (cs + 1 ● cs3 + 1)) -IHA
   /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
 | #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20
   elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct