-| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #d #HL #H
- elim (lsx_inv_bind … H) -H
- /4 width=9 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
-| #G #L #V #T1 #T2 #_ #IHT12 #d #HL #H
+| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #l #HL #H
+ elim (lsx_inv_bind … H) -H #HV #HU1
+ <(ypred_succ l) <yminus_SO2
+ /4 width=7 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
+| #G #L #V #T1 #T2 #_ #IHT12 #l #HL #H