-lemma lifts_lift_trans: ∀des,i,i0. @[i] des ≡ i0 →
+lemma lifts_lift_trans: ∀des,i,i0. @⦃i, des⦄ ≡ i0 →
∀des0. des + 1 ▭ i + 1 ≡ des0 + 1 →
∀T1,T0. ⇧*[des0] T1 ≡ T0 →
∀T2. ⇧[O, i0 + 1] T0 ≡ T2 →
∀des0. des + 1 ▭ i + 1 ≡ des0 + 1 →
∀T1,T0. ⇧*[des0] T1 ≡ T0 →
∀T2. ⇧[O, i0 + 1] T0 ≡ T2 →