- nDestructTac: Sys.break handled in two places

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

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 dff92c9503bcc329a91b0c345388f9c9a26e9315..1805953b99870cee59fa5328d9a3990cbd8afff1 100644 (file)
--- 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.