+
+(* Advanced inversion lemma *************************************************)
+
+lemma drops_inv_x_pair_xy: ∀b,f,I,L,V. ⬇*[b,f] L ≡ L.ⓑ{I}V → ⊥.
+#b #f #I #L #V #H lapply (drops_fwd_lw … H) -b -f
+/2 width=4 by lt_le_false/ (**) (* full auto is a bit slow: 19s *)
+qed-.