-lemma csx_ind_alt: ∀h,o,G,L. ∀R:predicate term.
- (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
- ) →
- ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
-#h #o #G #L #R #IH #T #HT
-@(csx_ind_cpxs_tdeq … IH … HT) -IH -HT // (**) (* full auto fails *)
+(* Basic_2A1: was: csx_ind_alt *)
+lemma csx_ind_cpxs: ∀h,G,L. ∀Q:predicate term.
+ (∀T1. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T1❫ →
+ (∀T2. ❪G,L❫ ⊢ T1 ⬈*[h] T2 → (T1 ≛ T2 → ⊥) → Q T2) → Q T1
+ ) →
+ ∀T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪T❫ → Q T.
+#h #G #L #Q #IH #T #HT
+@(csx_ind_cpxs_teqx … IH … HT) -IH -HT // (**) (* full auto fails *)