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