-lemma nlift_inv_bind: ∀a,I,W,U,d,e. (∀X. ⬆[d, e] X ≡ ⓑ{a,I}W.U → ⊥) →
- (∀V. ⬆[d, e] V ≡ W → ⊥) ∨ (∀T. ⬆[d+1, e] T ≡ U → ⊥).
-#a #I #W #U #d #e #H elim (is_lift_dec W d e)
+lemma nlift_inv_bind: ∀a,I,W,U,l,m. (∀X. ⬆[l, m] X ≡ ⓑ{a,I}W.U → ⊥) →
+ (∀V. ⬆[l, m] V ≡ W → ⊥) ∨ (∀T. ⬆[l+1, m] T ≡ U → ⊥).
+#a #I #W #U #l #m #H elim (is_lift_dec W l m)