-lemma lprs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 →
- (â\88\80L1,L. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h] L â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\9e¡*[h] L2 â\86\92 R L â\86\92 R L1) →
- â\88\80L1. â¦\83G, L1â¦\84 â\8a¢ â\9e¡*[h] L2 â\86\92 R L1.
+lemma lprs_ind_sn (h) (G) (L2): ∀Q:predicate lenv. Q L2 →
+ (â\88\80L1,L. â\9dªG,L1â\9d« â\8a¢ â\9e¡[h] L â\86\92 â\9dªG,Lâ\9d« â\8a¢ â\9e¡*[h] L2 â\86\92 Q L â\86\92 Q L1) →
+ â\88\80L1. â\9dªG,L1â\9d« â\8a¢ â\9e¡*[h] L2 â\86\92 Q L1.