X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Facp_cr.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Facp_cr.ma;h=1805953b99870cee59fa5328d9a3990cbd8afff1;hb=5ac2dc4e01aca542ddd13c02b304c646d8df9799;hp=dff92c9503bcc329a91b0c345388f9c9a26e9315;hpb=a386e0eb6b20909ae78c825203d77647b8fde30c;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 dff92c950..1805953b9 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
@@ -27,7 +27,7 @@ definition S1 ≝ λRP,C:lenv→predicate term.
 (* Note: this is Tait's iii, or Girard's CR4 *)
 definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term.
                 ∀L,Vs. all … (RP L) Vs →
-                ∀T. 𝐒[T] → NF … (RR L) RS T → C L (ⒶVs.T).
+                ∀T. 𝐒⦃T⦄ → NF … (RR L) RS T → C L (ⒶVs.T).
 
 (* Note: this is Tait's ii *)
 definition S3 ≝ λRP,C:lenv→predicate term.