-lemma rpx_inv_lpx_req: â\88\80h,G,L1,L2,T. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] L2 →
- â\88\83â\88\83L. â¦\83G, L1â¦\84 ⊢ ⬈[h] L & L ≡[T] L2.
+lemma rpx_inv_lpx_req: â\88\80h,G,L1,L2,T. â\9dªG,L1â\9d« â\8a¢ â¬\88[h,T] L2 →
+ â\88\83â\88\83L. â\9dªG,L1â\9d« ⊢ ⬈[h] L & L ≡[T] L2.