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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_trans.ma
index 2ff1bbb6d..67104bbc6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_trans.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_teqx_trans.ma
@@ -19,9 +19,9 @@ include "basic_2/dynamic/cnv_cpm_teqx.ma".
 
 definition IH_cnv_cpm_teqx_cpm_trans (h) (a): relation3 genv lenv term ≝
            λG,L,T1. ❪G,L❫ ⊢ T1 ![h,a] →
-           ∀n1,T. ❪G,L❫ ⊢ T1 ➡[n1,h] T → T1 ≛ T →
-           ∀n2,T2. ❪G,L❫ ⊢ T ➡[n2,h] T2 →
-           ∃∃T0. ❪G,L❫ ⊢ T1 ➡[n2,h] T0 & ❪G,L❫ ⊢ T0 ➡[n1,h] T2 & T0 ≛ T2.
+           ∀n1,T. ❪G,L❫ ⊢ T1 ➡[h,n1] T → T1 ≛ T →
+           ∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 →
+           ∃∃T0. ❪G,L❫ ⊢ T1 ➡[h,n2] T0 & ❪G,L❫ ⊢ T0 ➡[h,n1] T2 & T0 ≛ T2.
 
 (* Transitive properties restricted rt-transition for terms *****************)