-lemma drops_split_trans_bind2: â\88\80b,f,I,L,K0. â¬\87*[b, f] L â\89¡ K0.â\93\98{I} â\86\92 â\88\80i. @â¦\83O, fâ¦\84 â\89¡ i →
- â\88\83â\88\83J,K. â¬\87*[i]L â\89¡ K.â\93\98{J} & â¬\87*[b, ⫱*[⫯i]f] K â\89¡ K0 & â¬\86*[⫱*[⫯i]f] I â\89¡ J.
+lemma drops_split_trans_bind2: â\88\80b,f,I,L,K0. â¬\87*[b, f] L â\89\98 K0.â\93\98{I} â\86\92 â\88\80i. @â¦\83O, fâ¦\84 â\89\98 i →
+ â\88\83â\88\83J,K. â¬\87*[i]L â\89\98 K.â\93\98{J} & â¬\87*[b, ⫱*[â\86\91i]f] K â\89\98 K0 & â¬\86*[⫱*[â\86\91i]f] I â\89\98 J.