-lemma drops_inv_bind2_isuni: â\88\80b,f,I,K,L1. ð\9d\90\94â¦\83fâ¦\84 â\86\92 â¬\87*[b, f] L1 â\89\98 K.â\93\98{I} →
- (ð\9d\90\88â¦\83fâ¦\84 â\88§ L1 = K.â\93\98{I}) ∨
- â\88\83â\88\83g,I1,K1. ð\9d\90\94â¦\83gâ¦\84 & â¬\87*[b, g] K1 â\89\98 K.â\93\98{I} & L1 = K1.â\93\98{I1} & f = ↑g.
+lemma drops_inv_bind2_isuni: â\88\80b,f,I,K,L1. ð\9d\90\94â\9dªfâ\9d« â\86\92 â\87©*[b,f] L1 â\89\98 K.â\93\98[I] →
+ (ð\9d\90\88â\9dªfâ\9d« â\88§ L1 = K.â\93\98[I]) ∨
+ â\88\83â\88\83g,I1,K1. ð\9d\90\94â\9dªgâ\9d« & â\87©*[b,g] K1 â\89\98 K.â\93\98[I] & L1 = K1.â\93\98[I1] & f = ↑g.