-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
+lemma fsb_inv_csx: ∀h,G,L,T. ≥[h] 𝐒⦃G, L, T⦄ → ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+#h #G #L #T #H @(fsb_ind_alt … H) -G -L -T /5 width=1 by csx_intro, fpb_cpx/
+qed-.
+
+(* Propreties with context-sensitive stringly rt-normalizing terms **********)
+
+lemma csx_fsb_fpbs: ∀h,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h] ⦃G2, L2, T2⦄ → ≥[h] 𝐒⦃G2, L2, T2⦄.
+#h #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
+@(rdsx_ind … (csx_rdsx … HT0)) -L0