X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpx.ma;h=9e9dcf7b2e23a9e95e5616f1a221e5c72649d2f3;hp=13e3a4230fb5e03800ae041d72cc55b19a018d14;hb=e23331eef5817eaa6c5e1c442d1d6bbb18650573;hpb=b118146b97959e6a6dde18fdd014b8e1e676a2d1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
index 13e3a4230..9e9dcf7b2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
@@ -24,10 +24,8 @@ include "basic_2/rt_transition/cpg.ma".
 
 (* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS **************)
 
-definition sort_eq_f: relation nat ≝ λs1,s2. ⊤.
-
 definition cpx (G) (L): relation2 term term ≝
-           λT1,T2. ∃c. ❪G,L❫ ⊢ T1 ⬈[sort_eq_f,rtc_eq_f,c] T2.
+           λT1,T2. ∃c. ❪G,L❫ ⊢ T1 ⬈[sfull,rtc_eq_f,c] T2.
 
 interpretation
   "extended context-sensitive parallel rt-transition (term)"