update in basic_2 and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cnuw.ma

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 a02ea47dfaf53b0a36d0f2abb8b15cffabbe65fa..b47d310e8c692ba3c767f502c72e52a1e39758fb 100644 (file)
--- 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)"