X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Facp.ma;h=b7b967e1a2df51b34b165645011db12829f52202;hb=132d053caaeb9f8311fb0c807a9d7fd8d7acc827;hp=dc046b094990e20180b2f8ee38cd2c5d945ca5f1;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma
index dc046b094..b7b967e1a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma
@@ -26,7 +26,7 @@ definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term.
                  ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V.
 
 definition CP4 ≝ λRR:lenv→relation term. λRS:relation term.
-                 ∀L0,L,T,T0,d,e. NF … (RR L) RS T → 
+                 ∀L0,L,T,T0,d,e. NF … (RR L) RS T →
                  ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR L0) RS T0.
 
 definition CP4s ≝ λRR:lenv→relation term. λRS:relation term.