-lemma cpxs_tneqx_fwd_step_sn: ∀h,G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) →
- ∃∃T,T0. ⦃G,L⦄ ⊢ T1 ⬈[h] T & T1 ≛ T → ⊥ & ⦃G,L⦄ ⊢ T ⬈*[h] T0 & T0 ≛ T2.
-#h #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
+lemma cpxs_tneqx_fwd_step_sn (G) (L):
+ ∀T1,T2. ❪G,L❫ ⊢ T1 ⬈* T2 → (T1 ≛ T2 → ⊥) →
+ ∃∃T,T0. ❪G,L❫ ⊢ T1 ⬈ T & T1 ≛ T → ⊥ & ❪G,L❫ ⊢ T ⬈* T0 & T0 ≛ T2.
+#G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1