-lemma frees_inv_lref_drops: ∀L,i,f. L ⊢ 𝐅*⦃#i⦄ ≘ f →
- ∨∨ ∃∃g. ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ & 𝐈⦃g⦄ & f = ⫯*[i] ↑g
- | ∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≘ g &
- ⬇*[i] L ≘ K.ⓑ{I}V & f = ⫯*[i] ↑g
- | ∃∃g,I,K. ⬇*[i] L ≘ K.ⓤ{I} & 𝐈⦃g⦄ & f = ⫯*[i] ↑g.
+lemma frees_inv_lref_drops:
+ ∀L,i,f. L ⊢ 𝐅+⦃#i⦄ ≘ f →
+ ∨∨ ∃∃g. ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ & 𝐈⦃g⦄ & f = ⫯*[i] ↑g
+ | ∃∃g,I,K,V. K ⊢ 𝐅+⦃V⦄ ≘ g & ⬇*[i] L ≘ K.ⓑ{I}V & f = ⫯*[i] ↑g
+ | ∃∃g,I,K. ⬇*[i] L ≘ K.ⓤ{I} & 𝐈⦃g⦄ & f = ⫯*[i] ↑g.