-lemma lprs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 →
- (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → ⦃G, L⦄ ⊢ ➡*[h] L2 → R L → R L1) →
- ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L1.
+lemma lprs_ind_sn (h) (G) (L2): ∀Q:predicate lenv. Q L2 →
+ (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → ⦃G, L⦄ ⊢ ➡*[h] L2 → Q L → Q L1) →
+ ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → Q L1.