-lemma drops_lreq_trans_next: â\88\80f1,K1,K2. K1 â\89\90[f1] K2 →
- â\88\80b,f,I,L1. â¬\87*[b, f] L1.â\93\98{I} â\89¡ K1 →
- â\88\80f2. f ~â\8a\9a f1 â\89¡ ⫯f2 →
- â\88\83â\88\83L2. â¬\87*[b, f] L2.â\93\98{I} â\89¡ K2 & L1 â\89\90[f2] L2 & L1.â\93\98{I} â\89\90[f] L2.ⓘ{I}.
+lemma drops_lreq_trans_next: â\88\80f1,K1,K2. K1 â\89¡[f1] K2 →
+ â\88\80b,f,I,L1. â¬\87*[b, f] L1.â\93\98{I} â\89\98 K1 →
+ â\88\80f2. f ~â\8a\9a f1 â\89\98 â\86\91f2 →
+ â\88\83â\88\83L2. â¬\87*[b, f] L2.â\93\98{I} â\89\98 K2 & L1 â\89¡[f2] L2 & L1.â\93\98{I} â\89¡[f] L2.ⓘ{I}.