X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcnuw.ma;h=b47d310e8c692ba3c767f502c72e52a1e39758fb;hp=a02ea47dfaf53b0a36d0f2abb8b15cffabbe65fa;hb=ca7327c20c6031829fade8bb84a3a1bb66113f54;hpb=25c634037771dff0138e5e8e3d4378183ff49b86

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma
index a02ea47df..b47d310e8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cnuw.ma
@@ -19,7 +19,7 @@ include "basic_2/rt_computation/cpms.ma".
 (* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
 
 definition cnuw (h) (G) (L): predicate term ≝
-           λT1. ∀n,T2. ❪G,L❫ ⊢ T1 ➡*[n,h] T2 → T1 ≅ T2.
+           λT1. ∀n,T2. ❪G,L❫ ⊢ T1 ➡*[h,n] T2 → T1 ≅ T2.
 
 interpretation
   "normality for t-unbound weak head context-sensitive parallel rt-transition (term)"