-lemma drops_bind2_fwd_rfw: â\88\80b,f,I,L,K,V. â¬\87*[b, f] L â\89\98 K.â\93\91{I}V â\86\92 â\88\80T. â\99¯{K, V} < â\99¯{L, T}.
+lemma drops_bind2_fwd_rfw: â\88\80b,f,I,L,K,V. â\87©*[b,f] L â\89\98 K.â\93\91[I]V â\86\92 â\88\80T. â\99¯â\9d¨K,Vâ\9d© < â\99¯â\9d¨L,Tâ\9d©.