+theorem vlift_swap (M): ∀i1,i2. i1 ≤ i2 →
+ ∀lv,d1,d2. ⫯[i1←d1] ⫯[i2←d2] lv ≐{?,dd M} ⫯[↑i2←d2] ⫯[i1←d1] lv.
+#M #i1 #i2 #Hi12 #lv #d1 #d2 #j
+elim (lt_or_eq_or_gt j i1) #Hji1 destruct
+[ >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/
+ ]
+]
+qed-.
+