milestone update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpx.ma

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 13e3a4230fb5e03800ae041d72cc55b19a018d14..9e9dcf7b2e23a9e95e5616f1a221e5c72649d2f3 100644 (file)
--- 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)"