-lemma rsx_rdeq_trans (h) (G):
- â\88\80L1,T. G â\8a¢ â¬\88*[h,T] ð\9d\90\92â¦\83L1â¦\84 →
- â\88\80L2. L1 â\89\9b[T] L2 â\86\92 G â\8a¢ â¬\88*[h,T] ð\9d\90\92â¦\83L2â¦\84.
+lemma rsx_reqx_trans (h) (G):
+ â\88\80L1,T. G â\8a¢ â¬\88*[h,T] ð\9d\90\92â\9dªL1â\9d« →
+ â\88\80L2. L1 â\89\9b[T] L2 â\86\92 G â\8a¢ â¬\88*[h,T] ð\9d\90\92â\9dªL2â\9d«.