-lemma csx_ind_cpxs_teqx: ∀h,G,L. ∀Q:predicate term.
- (∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
- ) →
- ∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
- ∀T0. ❪G,L❫ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛ T2 → Q T2.
-#h #G #L #Q #IH #T1 #H @(csx_ind … H) -T1
+lemma csx_ind_cpxs_teqx (G) (L):
+ ∀Q:predicate term.
+ (∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈* T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
+ ) →
+ ∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
+ ∀T0. ❪G,L❫ ⊢ T1 ⬈* T0 → ∀T2. T0 ≛ T2 → Q T2.
+#G #L #Q #IH #T1 #H @(csx_ind … H) -T1