+(* Advanced inversion lemmas ************************************************)
+
+lemma lsubv_inv_abst_sn (a) (h) (G): ∀K1,L2,W. G ⊢ K1.ⓛW ⫃![a,h] L2 →
+ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓛW.
+#a #h #G #K1 #L2 #W #H
+elim (lsubv_inv_bind_sn … H) -H // *
+#K2 #XW #XV #_ #_ #H1 #H2 destruct
+qed-.
+