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=f79d97a42a84f94d37ad9589fcce46149ee23d12;hp=e25f2975fccd2702767f2b477a086e273f76fd22;hpb=2ba7ef901a6b72210692792f2396c08bc0cff52c;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 e25f2975f..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
@@ -26,8 +26,8 @@ include "basic_2/computation/lsubc_ldrops.ma".
 theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
                               acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
                               ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
-                              ∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 →
-                              ⦃L2, T0⦄ [RP] ϵ 〚A〛.
+                              ∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 ⊑[RP] L0 →
+                              ⦃L2, T0⦄ ϵ[RP] 〚A〛.
 #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
@@ -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
@@ -90,7 +90,7 @@ qed.
 
 (* Basic_1: was: sc3_arity *)
 lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
-                ∀L,T,A. L ⊢ T ⁝ A → ⦃L, T⦄ [RP] ϵ 〚A〛.
+                ∀L,T,A. L ⊢ T ⁝ A → ⦃L, T⦄ ϵ[RP] 〚A〛.
 /2 width=8/ qed.
 
 lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →