elim (teqx_dec T0 T4) [ -IHc -HT04 #HT04 | -IHu #HnT04 ]
[ elim (teqx_fqup_trans … H43 … HT04) -T4 #L2 #T4 #H04 #HT43 #HL24
/4 width=7 by fsb_fpbs_trans, teqx_reqx_lpx_fpbs, fpbs_fqup_trans/
elim (teqx_dec T0 T4) [ -IHc -HT04 #HT04 | -IHu #HnT04 ]
[ elim (teqx_fqup_trans … H43 … HT04) -T4 #L2 #T4 #H04 #HT43 #HL24
/4 width=7 by fsb_fpbs_trans, teqx_reqx_lpx_fpbs, fpbs_fqup_trans/