-lemma frees_inv_lift_be: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
- ∀K,s,d0,e0. ⬇[s, d0, e0+1] L ≡ K →
- ∀T. ⬆[d0, e0+1] T ≡ U → d0 ≤ i → i ≤ d0 + e0 → ⊥.
-#L #U #d #i #H elim H -L -U -d -i
-[ #L #U #d #i #HnU #K #s #d0 #e0 #_ #T #HTU #Hd0i #Hide0
- elim (lift_split … HTU i e0) -HTU /2 width=2 by/
-| #I #L #K0 #U #W #d #i #j #Hdi #Hij #HnU #HLK0 #_ #IHW #K #s #d0 #e0 #HLK #T #HTU #Hd0i #Hide0
- elim (lt_or_ge j d0) #H1
+lemma frees_inv_lift_be: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
+ ∀K,s,l0,m0. ⬇[s, l0, m0+1] L ≡ K →
+ ∀T. ⬆[l0, m0+1] T ≡ U → l0 ≤ i → i ≤ l0 + m0 → ⊥.
+#L #U #l #i #H elim H -L -U -l -i
+[ #L #U #l #i #HnU #K #s #l0 #m0 #_ #T #HTU #Hl0i #Hilm0
+ elim (lift_split … HTU i m0) -HTU /2 width=2 by/
+| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hl0i #Hilm0
+ elim (lt_or_ge j l0) #H1