-theorem liftsv_trans: ∀T1s,Ts,t1. ⬆*[t1] T1s ≡ Ts → ∀T2s,t2. ⬆*[t2] Ts ≡ T2s →
- ∀t. t2 ⊚ t1 ≡ t → ⬆*[t] T1s ≡ T2s.
-#T1s #Ts #t1 #H elim H -T1s -Ts
-[ #T2s #t2 #H >(liftsv_inv_nil1 … H) -T2s /2 width=3 by liftsv_nil/
-| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #t2 #H elim (liftsv_inv_cons1 … H) -H
+theorem liftsv_trans: ∀f1,T1s,Ts. ⬆*[f1] T1s ≘ Ts → ∀T2s,f2. ⬆*[f2] Ts ≘ T2s →
+ ∀f. f2 ⊚ f1 ≘ f → ⬆*[f] T1s ≘ T2s.
+#f1 #T1s #Ts #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