#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
#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
[ /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/
[ /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/
[ /3 width=3 by fpbs_lpxs_trans, lpx_lpxs/
| #G3 #L3 #T3 #H03 #_ elim (lpx_fqup_trans … H03 … HL02) -L2
#L4 #T4 elim (eq_term_dec T0 T4) [ -IHc | -IHu ]
[ /3 width=3 by fpbs_lpxs_trans, lpx_lpxs/
| #G3 #L3 #T3 #H03 #_ elim (lpx_fqup_trans … H03 … HL02) -L2
#L4 #T4 elim (eq_term_dec T0 T4) [ -IHc | -IHu ]