- elim (lt_or_ge i (j+1)) #Hji
- [ -IH elim (frees_inv_lift_be … H2 … HLK2 … HW0U2) /2 width=1 by monotonic_pred/
- | lapply (frees_inv_lift_ge … H2 … HLK2 … HW0U2 ?) -L2 -U2 // <minus_plus destruct
- /4 width=11 by frees_lref_be, fqup_lref/
+ elim (ylt_split i (j+1)) >yplus_SO2 #Hji
+ [ -IH elim (frees_inv_lift_be … H2 … HLK2 … HW0U2) /2 width=1 by ylt_fwd_succ2/
+ | lapply (frees_inv_lift_ge … H2 … HLK2 … HW0U2 ?) -L2 -U2 // destruct
+ /4 width=11 by frees_lref_be, fqup_lref, yle_succ1_inj/