-lemma rpx_inv_lpx_req: â\88\80h,G,L1,L2,T. â¦\83G,L1â¦\84 ⊢ ⬈[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« ⊢ ⬈[h,T] L2 →
+ â\88\83â\88\83L. â\9dªG,L1â\9d« ⊢ ⬈[h] L & L ≡[T] L2.