-lemma lifts_applv: ∀V1s,V2s,des. ⬆*[des] V1s ≡ V2s →
- ∀T1,T2. ⬆*[des] T1 ≡ T2 →
- ⬆*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
-#V1s #V2s #des #H elim H -V1s -V2s /3 width=1 by lifts_flat/
+lemma lifts_applv: ∀V1s,V2s,cs. ⬆*[cs] V1s ≡ V2s →
+ ∀T1,T2. ⬆*[cs] T1 ≡ T2 →
+ ⬆*[cs] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
+#V1s #V2s #cs #H elim H -V1s -V2s /3 width=1 by lifts_flat/