-lemma csx_fsb_fpbs: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦥[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #L1 #T1 #H @(csx_ind … H) -T1
-#T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind … G2 L2 T2) -G2 -L2 -T2
-#G0 #L0 #T0 #IHu #H10 lapply (csx_fpbs_conf … H10) // -HT1
-#HT0 generalize in match IHu; -IHu generalize in match H10; -H10
-@(lsx_ind … (csx_lsx … HT0 0)) -L0
-#L0 #_ #IHd #H10 #IHu @fsb_intro
-#G2 #L2 #T2 * -G2 -L2 -T2 [ -IHd -IHc | -IHu -IHd | ]
-[ /4 width=5 by fpbs_fqup_trans, fqu_fqup/
-| #T2 #HT02 #HnT02 elim (fpbs_cpx_trans_neq … H10 … HT02 HnT02) -T0
- /3 width=4 by/
-| #L2 #HL02 #HnL02 @(IHd … HL02 HnL02) -IHd -HnL02 [ -IHu -IHc | ]
+lemma fsb_inv_csx:
+ ∀G,L,T. ≥𝐒 ❪G,L,T❫ → ❪G,L❫ ⊢ ⬈*𝐒 T.
+#G #L #T #H @(fsb_ind_alt … H) -G -L -T
+/5 width=1 by csx_intro, cpx_fpbc/
+qed-.
+
+(* Propreties with context-sensitive stringly rt-normalizing terms **********)
+
+lemma csx_fsb_fpbs:
+ ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
+ ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫.
+#G1 #L1 #T1 #H @(csx_ind … H) -T1
+#T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind (Ⓣ) … G2 L2 T2) -G2 -L2 -T2
+#G0 #L0 #T0 #IHu #H10
+lapply (fpbs_csx_conf … H10) // -HT1 #HT0
+generalize in match IHu; -IHu generalize in match H10; -H10
+@(rsx_ind … (csx_rsx … HT0)) -L0 #L0 #_ #IHd #H10 #IHu
+@fsb_intro #G2 #L2 #T2 #H
+elim (fpbc_fwd_lpx … H) -H * [ -IHd -IHc | -IHu -IHd |]
+[ /5 width=5 by fsb_fpb_trans, fpbs_fqup_trans, fqu_fqup/
+| #T3 #HT03 #HnT03 #H32
+ elim (fpbs_cpx_tneqg_trans … H10 … HT03 HnT03) -T0
+ /4 width=5 by fsb_fpb_trans, sfull_dec/
+| #L3 #HL03 #HnL03 #HL32
+ @(fsb_fpb_trans … HL32) -L2
+ @(IHd … HL03 HnL03) -IHd -HnL03 [ -IHu -IHc |]