-lemma csx_ind: ∀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 #H0 #T1 #H elim H -T1
+lemma csx_ind (G) (L) (Q:predicate …):
+ (∀T1. ❨G,L❩ ⊢ ⬈*𝐒 T1 →
+ (∀T2. ❨G,L❩ ⊢ T1 ⬈ T2 → (T1 ≅ T2 → ⊥) → Q T2) →
+ Q T1
+ ) →
+ ∀T. ❨G,L❩ ⊢ ⬈*𝐒 T → Q T.
+#G #L #Q #H0 #T1 #H elim H -T1