(* Main properties **********************************************************)
-(* Basic_1: was: lifts1_xhg *)
+(* Basic_1: was: lifts1_xhg (right to left) *)
lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts →
∀T2s:list term. ⇧[0, 1] Ts ≡ T2s →
∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[des + 1] T0s ≡ T2s.