(* Main properties **********************************************************)
-(* Basic_1: was: lift1_lift1 (left to right) *)
theorem lifts_trans: ∀T1,T,cs1. ⬆*[cs1] T1 ≡ T → ∀T2:term. ∀cs2. ⬆*[cs2] T ≡ T2 →
⬆*[cs1 @@ cs2] T1 ≡ T2.
#T1 #T #cs1 #H elim H -T1 -T -cs1 /3 width=3 by lifts_cons/