(* Main properties **********************************************************)
theorem lifts_trans: ∀T1,T,cs1. ⬆*[cs1] T1 ≡ T → ∀T2:term. ∀cs2. ⬆*[cs2] T ≡ T2 →
- ⬆*[cs1 ;; cs2] T1 ≡ T2.
+ ⬆*[cs1 ● cs2] T1 ≡ T2.
#T1 #T #cs1 #H elim H -T1 -T -cs1 /3 width=3 by lifts_cons/
qed.