-lemma lprs_pair (h) (G): â\88\80L1,L2. â¦\83G,L1â¦\84 â\8a¢ â\9e¡*[h] L2 →
- â\88\80V1,V2. â¦\83G,L1â¦\84 â\8a¢ V1 â\9e¡*[h] V2 →
- â\88\80I. â¦\83G,L1.â\93\91{I}V1â¦\84 â\8a¢ â\9e¡*[h] L2.â\93\91{I}V2.
+lemma lprs_pair (h) (G): â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â\9e¡*[h,0] L2 →
+ â\88\80V1,V2. â\9dªG,L1â\9d« â\8a¢ V1 â\9e¡*[h,0] V2 →
+ â\88\80I. â\9dªG,L1.â\93\91[I]V1â\9d« â\8a¢ â\9e¡*[h,0] L2.â\93\91[I]V2.