| frees_sort: ∀f,L,s. 𝐈❪f❫ → frees L (⋆s) f
| frees_atom: ∀f,i. 𝐈❪f❫ → frees (⋆) (#i) (⫯*[i]↑f)
| frees_pair: ∀f,I,L,V. frees L V f →
| frees_sort: ∀f,L,s. 𝐈❪f❫ → frees L (⋆s) f
| frees_atom: ∀f,i. 𝐈❪f❫ → frees (⋆) (#i) (⫯*[i]↑f)
| frees_pair: ∀f,I,L,V. frees L V f →