| 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 →
f1 ⋓ ⫱f2 ≘ f → frees L (ⓑ{p,I}V.T) 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 →
f1 ⋓ ⫱f2 ≘ f → frees L (ⓑ{p,I}V.T) f