-| 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 →
+| frees_gref: ∀f,I,L,V,l. frees L (§l) f →
+ frees (L.ⓑ{I}V) (§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 →