X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fequivalence%2Fcpcs.ma;h=55bae3317c00245a23c3cf2df84d80e8c03c8dd1;hp=ffae53ad73a0425c75da8187f113e32a78af57b8;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2A/equivalence/cpcs.ma
index ffae53ad7..55bae3317 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/equivalence/cpcs.ma
@@ -18,7 +18,7 @@ include "basic_2A/conversion/cpc.ma".
 (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
 
 definition cpcs: relation4 genv lenv term term ≝
-           λG. LTC … (cpc G).
+           λG. CTC … (cpc G).
 
 interpretation "context-sensitive parallel equivalence (term)"
    'PConvStar G L T1 T2 = (cpcs G L T1 T2).