-@(rsx_ind … (csx_rsx … HT0)) -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_tneqx_trans … H10 … HT02 HnT02) -T0
- /3 width=4 by/
-| #L2 #HL02 #HnL02 @(IHd … HL02 HnL02) -IHd -HnL02 [ -IHu -IHc | ]
+@(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 |]