-lemma cpr_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
- â\88\80L2. L2 â\89¼ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
-#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
-lapply (tpss_lsubs_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/
+lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 →
+ â\88\80L2. L2 â\8a\91 [0, |L1|] L1 → L2 ⊢ T1 ➡ T2.
+#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
+lapply (tpss_lsubr_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/