-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/
+qed-.
+
+(* Advanced inversion lemma *************************************************)
+
+lemma drops_inv_x_bind_xy: ∀b,f,I,L. ⬇*[b, f] L ≘ L.ⓘ{I} → ⊥.
+#b #f #I #L #H lapply (drops_fwd_lw … H) -b -f
+/2 width=4 by lt_le_false/ (**) (* full auto is a bit slow: 19s *)