-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.
+lemma lprs_ind_sn (h) (G) (L2):
+ ∀Q:predicate lenv. Q L2 →
+ (∀L1,L. ❪G,L1❫ ⊢ ➡[h,0] L → ❪G,L❫ ⊢ ➡*[h,0] L2 → Q L → Q L1) →
+ ∀L1. ❪G,L1❫ ⊢ ➡*[h,0] L2 → Q L1.