-lemma cpcs_ind_sn (h): ∀G,L,T2. ∀R:predicate term. R T2 →
- (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) →
- ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1.
+lemma cpcs_ind_sn (h) (G) (L) (T2):
+ ∀Q:predicate term. Q T2 →
+ (∀T1,T. ❨G,L❩ ⊢ T1 ⬌[h] T → ❨G,L❩ ⊢ T ⬌*[h] T2 → Q T → Q T1) →
+ ∀T1. ❨G,L❩ ⊢ T1 ⬌*[h] T2 → Q T1.