-[ >vlift_lt // >vlift_lt /2 width=3 by lt_to_le_to_lt/
- >vlift_lt /3 width=3 by lt_S, lt_to_le_to_lt/ >vlift_lt //
-| >vlift_eq >vlift_lt /2 width=1 by monotonic_le_plus_l/ >vlift_eq //
-| >vlift_gt // elim (lt_or_eq_or_gt (↓j) i2) #Hji2 destruct
- [ >vlift_lt // >vlift_lt /2 width=1 by lt_minus_to_plus/ >vlift_gt //
- | >vlift_eq <(lt_succ_pred … Hji1) >vlift_eq //
- | >vlift_gt // >vlift_gt /2 width=1 by lt_minus_to_plus_r/ >vlift_gt /2 width=3 by le_to_lt_to_lt/
+[ lapply (lt_to_le_to_lt … Hji1 Hi12) #Hji2
+ >vpush_lt // >vpush_lt // >vpush_lt /2 width=1 by lt_S/ >vpush_lt //
+ /2 width=1 by veq_refl/
+| >vpush_eq >vpush_lt /2 width=1 by monotonic_le_plus_l/ >vpush_eq
+ /2 width=1 by mr/
+| >vpush_gt // elim (lt_or_eq_or_gt (↓j) i2) #Hji2 destruct
+ [ >vpush_lt // >vpush_lt /2 width=1 by lt_minus_to_plus/ >vpush_gt //
+ /2 width=1 by veq_refl/
+ | >vpush_eq <(lt_succ_pred … Hji1) >vpush_eq
+ /2 width=1 by mr/
+ | lapply (le_to_lt_to_lt … Hi12 Hji2) #Hi1j
+ >vpush_gt // >vpush_gt /2 width=1 by lt_minus_to_plus_r/ >vpush_gt //
+ /2 width=1 by veq_refl/