-lemma drops_inv_bind2_isuni: â\88\80b,f,I,K,L1. ð\9d\90\94â\9dªfâ\9d« → ⇩*[b,f] L1 ≘ K.ⓘ[I] →
- (ð\9d\90\88â\9dªfâ\9d« ∧ L1 = K.ⓘ[I]) ∨
- â\88\83â\88\83g,I1,K1. ð\9d\90\94â\9dªgâ\9d« & ⇩*[b,g] K1 ≘ K.ⓘ[I] & L1 = K1.ⓘ[I1] & f = ↑g.
+lemma drops_inv_bind2_isuni: â\88\80b,f,I,K,L1. ð\9d\90\94â\9d¨fâ\9d© → ⇩*[b,f] L1 ≘ K.ⓘ[I] →
+ (ð\9d\90\88â\9d¨fâ\9d© ∧ L1 = K.ⓘ[I]) ∨
+ â\88\83â\88\83g,I1,K1. ð\9d\90\94â\9d¨gâ\9d© & ⇩*[b,g] K1 ≘ K.ⓘ[I] & L1 = K1.ⓘ[I1] & f = ↑g.