-lemma cprs_ind_sn (h) (G) (L) (T2) (R:predicate …):
- 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.
-#h #G #L #T2 #R #IH1 #IH2 #T1
+lemma cprs_ind_sn (h) (G) (L) (T2) (Q:predicate …):
+ 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.
+#h #G #L #T2 #Q #IH1 #IH2 #T1