-| frees_atom: ∀I,f. 𝐈⦃f⦄ → frees (⋆) (⓪{I}) f
-| frees_sort: ∀I,L,V,s,f. frees L (⋆s) f →
- frees (L.ⓑ{I}V) (⋆s) (↑f)
-| frees_zero: ∀I,L,V,f. frees L V f →
- frees (L.ⓑ{I}V) (#0) (⫯f)
-| frees_lref: ∀I,L,V,i,f. frees L (#i) f →
- frees (L.ⓑ{I}V) (#⫯i) (↑f)
-| frees_gref: ∀I,L,V,p,f. frees L (§p) f →
- frees (L.ⓑ{I}V) (§p) (↑f)
-| frees_bind: ∀I,L,V,T,a,f1,f2,f. frees L V f1 → frees (L.ⓑ{I}V) T f2 →
- f1 ⋓ ⫱f2 ≡ f → frees L (ⓑ{a,I}V.T) f
-| frees_flat: ∀I,L,V,T,f1,f2,f. frees L V f1 → frees L T f2 →
- f1 ⋓ f2 ≡ f → frees L (ⓕ{I}V.T) 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 →
+ frees (L.ⓑ{I}V) (#0) (↑f)
+| frees_unit: ∀f,I,L. 𝐈⦃f⦄ → frees (L.ⓤ{I}) (#0) (↑f)
+| frees_lref: ∀f,I,L,i. frees L (#i) f →
+ 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 →
+ f1 ⋓ ⫱f2 ≘ f → frees L (ⓑ{p,I}V.T) f
+| frees_flat: ∀f1,f2,f,I,L,V,T. frees L V f1 → frees L T f2 →
+ f1 ⋓ f2 ≘ f → frees L (ⓕ{I}V.T) f