- we set up the support for the "bt-reduction" of Automath literature

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / acp_aaa.ma

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 1b2536c8b2b559a92cce195314fde89a0f14cc86..f4da11310f6e055a168f11605d84f7a1701344bb 100644 (file)
--- 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