definition IH_cnv_cpm_teqx_cpm_trans (h) (a): relation3 genv lenv term ≝
λG,L,T1. ❪G,L❫ ⊢ T1 ![h,a] →
- â\88\80n1,T. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n1] T â\86\92 T1 â\89\9b T →
+ â\88\80n1,T. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n1] T â\86\92 T1 â\89\85 T →
∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 →
- â\88\83â\88\83T0. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n2] T0 & â\9dªG,Lâ\9d« â\8a¢ T0 â\9e¡[h,n1] T2 & T0 â\89\9b T2.
+ â\88\83â\88\83T0. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n2] T0 & â\9dªG,Lâ\9d« â\8a¢ T0 â\9e¡[h,n1] T2 & T0 â\89\85 T2.
(* Transitive properties restricted rt-transition for terms *****************)
[ #H1 #H2 destruct /2 width=4 by ex3_intro/
| #s #H1 #H2 #H3 destruct
elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
- /3 width=4 by cpm_sort, teqx_sort, ex3_intro/
+ /3 width=4 by cpm_sort, teqg_sort, ex3_intro/
]
| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
elim (cpm_teqx_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #_ #H0T1 #H1T1 #H2T1 #H destruct