-lemma frees_inv: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
- (â\88\80T. â\87§[i, 1] T ≡ U → ⊥) ∨
- ∃∃I,K,W,j. d ≤ yinj j & j < i & (∀T. ⇧[j, 1] T ≡ U → ⊥) &
- â\87©[j]L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
-#L #U #d #i * -L -U -d -i /4 width=9 by ex5_4_intro, or_intror, or_introl/
+lemma frees_inv: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
+ (â\88\80T. â¬\86[i, 1] T ≡ U → ⊥) ∨
+ ∃∃I,K,W,j. l ≤ yinj j & j < i & (∀T. ⬆[j, 1] T ≡ U → ⊥) &
+ â¬\87[j]L ≡ K.ⓑ{I}W & K ⊢ (i-j-1) ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #U #l #i * -L -U -l -i /4 width=9 by ex5_4_intro, or_intror, or_introl/