-lemma drops_pair2_fwd_rfw: ∀I,L,K,V,c,f. ⬇*[c, f] L ≡ K.ⓑ{I}V → ∀T. ♯{K, V} < ♯{L, T}.
-#I #L #K #V #c #f #HLK lapply (drops_fwd_lw … HLK) -HLK
-normalize in ⊢ (%→?→?%%); /3 width=3 by le_to_lt_to_lt/
+lemma drops_bind2_fwd_rfw: ∀b,f,I,L,K,V. ⬇*[b, f] L ≘ K.ⓑ{I}V → ∀T. ♯{K, V} < ♯{L, T}.
+#b #f #I #L #K #V #HLK lapply (drops_fwd_lw … HLK) -HLK
+normalize in ⊢ (%→?→?%%); /3 width=3 by le_to_lt_to_lt, monotonic_lt_plus_r/