-lemma lifts_bind: ∀a,I,T2,V1,V2,des. ⬆*[des] V1 ≡ V2 →
- ∀T1. ⬆*[des + 1] T1 ≡ T2 →
- ⬆*[des] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
-#a #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
+lemma lifts_bind: ∀a,I,T2,V1,V2,cs. ⬆*[cs] V1 ≡ V2 →
+ ∀T1. ⬆*[cs + 1] T1 ≡ T2 →
+ ⬆*[cs] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
+#a #I #T2 #V1 #V2 #cs #H elim H -V1 -V2 -cs