lemma fsb_fpbs_trans:
∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫.
-#G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+#G1 #L1 #T1 #H @(fsb_ind … H) -G1 -L1 -T1
#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
elim (fpbs_inv_fpbg … H12) -H12
[ -IH /2 width=9 by fsb_feqg_trans/
) →
∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G2 L2 T2.
-#Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+#Q #IH1 #G1 #L1 #T1 #H @(fsb_ind … H) -G1 -L1 -T1
#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
@IH1 -IH1
[ -IH /2 width=5 by fsb_fpbs_trans/