-lemma csx_ind_cpxs_tdeq: ∀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.
+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.