- frees (L.ⓘ{I}) (#↑i) (⫯f)
-| frees_gref: â\88\80f,L,l. ð\9d\90\88â¦\83fâ¦\84 → 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 â\8b\93 ⫱f2 â\89\98 f â\86\92 frees L (â\93\91{p,I}V.T) f
+ frees (L.ⓘ[I]) (#↑i) (⫯f)
+| frees_gref: â\88\80f,L,l. ð\9d\90\88â\9d¨fâ\9d© → 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 â\8b\93 â«°f2 â\89\98 f â\86\92 frees L (â\93\91[p,I]V.T) f