-theorem liftsv_trans: ∀T1c,Ts,f1. ⬆*[f1] T1c ≡ Ts → ∀T2c,f2. ⬆*[f2] Ts ≡ T2c →
- ∀f. f2 ⊚ f1 ≡ f → ⬆*[f] T1c ≡ T2c.
-#T1c #Ts #f1 #H elim H -T1c -Ts
-[ #T2c #f2 #H >(liftsv_inv_nil1 … H) -T2c /2 width=3 by liftsv_nil/
-| #T1c #Ts #T1 #T #HT1 #_ #IHT1c #X #f2 #H elim (liftsv_inv_cons1 … H) -H
- #T2 #T2c #HT2 #HT2c #H destruct /3 width=6 by lifts_trans, liftsv_cons/
+theorem liftsv_trans: ∀T1s,Ts,f1. ⬆*[f1] T1s ≡ Ts → ∀T2s,f2. ⬆*[f2] Ts ≡ T2s →
+ ∀f. f2 ⊚ f1 ≡ f → ⬆*[f] T1s ≡ T2s.
+#T1s #Ts #f1 #H elim H -T1s -Ts
+[ #T2s #f2 #H >(liftsv_inv_nil1 … H) -T2s /2 width=3 by liftsv_nil/
+| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #f2 #H elim (liftsv_inv_cons1 … H) -H
+ #T2 #T2s #HT2 #HT2s #H destruct /3 width=6 by lifts_trans, liftsv_cons/