frees (L.ⓘ[I]) (#↑i) (⫯f)
| frees_gref: ∀f,L,l. 𝐈❪f❫ → frees L (§l) f
| frees_bind: ∀f1,f2,f,p,I,L,V,T. frees L V f1 → frees (L.ⓑ[I]V) T f2 →
frees (L.ⓘ[I]) (#↑i) (⫯f)
| frees_gref: ∀f,L,l. 𝐈❪f❫ → frees L (§l) f
| frees_bind: ∀f1,f2,f,p,I,L,V,T. frees L V f1 → frees (L.ⓑ[I]V) T f2 →