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 →