-lemma lreq_inv_push1: â\88\80g,J1,K1,Y. K1.â\93\98{J1} â\89¡[↑g] Y →
- â\88\83â\88\83J2,K2. K1 â\89¡[g] K2 & Y = K2.ⓘ{J2}.
+lemma lreq_inv_push1: â\88\80g,J1,K1,Y. K1.â\93\98{J1} â\89\90[↑g] Y →
+ â\88\83â\88\83J2,K2. K1 â\89\90[g] K2 & Y = K2.ⓘ{J2}.