+lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥.
+#h #g #L #T #U #l #H elim H -L -T -U -l
+[ #L #k #l #_ #H
+ elim (frsupp_inv_atom1_frsups … H)
+| #L #K #V #W #U #i #l #_ #_ #HWU #_ #H
+ elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H
+ elim (lift_inv_lref2_be … H ? ?) -H //
+| #L #K #W #V #U #i #l #_ #_ #HWU #_ #H
+ elim (lift_frsupp_trans … (⋆) … H … HWU) -U #X #H
+ elim (lift_inv_lref2_be … H ? ?) -H //
+| #a #I #L #V #T #U #l #_ #IHTU #H
+ elim (frsupp_inv_bind1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU
+ lapply (frsups_fwd_fw … H) -H normalize
+ <associative_plus <associative_plus #H
+ elim (le_plus_xySz_x_false … H)
+| #L #V #T #U #l #_ #IHTU #H
+ elim (frsupp_inv_flat1_frsups … H) -H #H [2: /4 width=4/ ] -IHTU
+ lapply (frsups_fwd_fw … H) -H normalize
+ <associative_plus <associative_plus #H
+ elim (le_plus_xySz_x_false … H)
+| /3 width=4/
+]
+qed-.
+