#h #G #L1 #T1 #T2 #HT12 #L2 #H
elim (tc_lfxs_inv_lex_lfeq … H) -H #L #HL1 #HL2
lapply (lfxs_lex … HL1 T1) #H
-elim (cpx_lfxs_conf_gen … HT12 … H) -HT12 -H // #_ #HT21 #_
+elim (cpx_lfxs_conf_fle … HT12 … H) -HT12 -H // #_ #HT21 #_
@(lfpxs_lpxs_lfeq … HL1) -HL1
@(fle_lfxs_trans … HL2) //
qed-.