-lemma fsb_inv_csx: ∀h,o,G,L,T. ⦥[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, o] T.
-#h #o #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpb_cpx/
+(* Note: eliminator with shorter ground hypothesis *)
+lemma fsb_ind (Q:relation3 …):
+ (∀G1,L1,T1. ≥𝐒 ❨G1,L1,T1❩ →
+ (∀G2,L2,T2. ❨G1,L1,T1❩ ≻ ❨G2,L2,T2❩ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) →
+ ∀G,L,T. ≥𝐒 ❨G,L,T❩ → Q G L T.
+#Q #IH #G #L #T #H elim H -G -L -T
+#G1 #L1 #T1 #H1 #IH1
+@IH -IH [ /4 width=1 by SN3_intro/ ] -H1 #G2 #L2 #T2 #H
+elim (fpbc_inv_gen sfull … H) -H #H12 #Hn12 /3 width=1 by/