-theorem liftsv_trans: ∀T1s,Ts,f1. ⬆*[f1] T1s ≡ Ts → ∀T2s,f2. ⬆*[f2] Ts ≡ T2s →
- â\88\80f. f2 â\8a\9a f1 â\89¡ f â\86\92 â¬\86*[f] T1s â\89¡ T2s.
-#T1s #Ts #f1 #H elim H -T1s -Ts
+theorem liftsv_trans: ∀f1,T1s,Ts. ⬆*[f1] T1s ≘ Ts → ∀T2s,f2. ⬆*[f2] Ts ≘ T2s →
+ â\88\80f. f2 â\8a\9a f1 â\89\98 f â\86\92 â¬\86*[f] T1s â\89\98 T2s.
+#f1 #T1s #Ts #H elim H -T1s -Ts