| #G3 #L3 #T3 #H03 #_
elim (lpx_fqup_trans … H03 … HL02) -L2 #L4 #T4 #HT04 #H43 #HL43
elim (teqx_dec T0 T4) [ -IHc -HT04 #HT04 | -IHu #HnT04 ]
| #G3 #L3 #T3 #H03 #_
elim (lpx_fqup_trans … H03 … HL02) -L2 #L4 #T4 #HT04 #H43 #HL43
elim (teqx_dec T0 T4) [ -IHc -HT04 #HT04 | -IHu #HnT04 ]