X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Facp_cr.ma;h=c45bc25914fbbef41fd70ef470ab1ce12b78a601;hb=a28bc89ee87228140c6559e3dacfeaaf2ac70d1d;hp=699d997dd2acb594e19f912772c364d45e4ec13b;hpb=30df7ebabc6eb145c28a9724c6e8ad9612c784b1;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
index 699d997dd..c45bc2591 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
@@ -88,11 +88,11 @@ axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
   @(s7 … IHA … HL21) [2: @HA [2: 
 ]
 qed.
-*)  
+*)
 lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
-                 ∀L,W,T,A,B. RP L W → 
-                 (∀V. {L, V} [RP] ϵ 〚B〛 → {L. 𝕓{Abbr}V, T} [RP] ϵ 〚A〛) →
-                 {L, 𝕓{Abst}W. T} [RP] ϵ 〚𝕔B. A〛.
+                 ∀L,W,T,A,B. RP L W →
+                 (∀V. ⦃L, V⦄ [RP] ϵ 〚B〛 → ⦃L. 𝕓{Abbr}V, T⦄ [RP] ϵ 〚A〛) →
+                              ⦃L, 𝕓{Abst}W. T⦄ [RP] ϵ 〚𝕔B. A〛.
 #RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #V #HB
 lapply (aacr_acr … H1RP H2RP A) #HCA
 lapply (aacr_acr … H1RP H2RP B) #HCB