- (∀n1,n2,T1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → ⦃G, L⦄ ⊢ T1 ![a,h] → T1 ≛[h,o] T → ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 → ⦃G, L⦄ ⊢ T ![a,h] → T ≛[h,o] T2 → Q n2 T → Q (n1+n2) T1) →
- ∀n,T1. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G, L⦄ ⊢ T1 ![a,h] → T1 ≛[h,o] T2 →
- (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
- (∀G0,L0,T0. ⦃G,L,T1⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
+ (∀n1,n2,T1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → ⦃G, L⦄ ⊢ T1 ![a,h] → T1 ≛ T → ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 → ⦃G, L⦄ ⊢ T ![a,h] → T ≛ T2 → Q n2 T → Q (n1+n2) T1) →
+ ∀n,T1. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G, L⦄ ⊢ T1 ![a,h] → T1 ≛ T2 →
+ (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
+ (∀G0,L0,T0. ⦃G,L,T1⦄ >[h] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →