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 â\8b\93 ⫱f2 ≘ f → frees L (ⓑ[p,I]V.T) f
+ f1 â\8b\93 â«°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
.
fact frees_inv_bind_aux:
∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀p,I,V,T. X = ⓑ[p,I]V.T →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 ⫱f2 ≘ f.
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
#f #L #X * -f -L -X
[ #f #L #s #_ #q #J #W #U #H destruct
| #f #i #_ #q #J #W #U #H destruct
lemma frees_inv_bind:
∀f,p,I,L,V,T. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f →
- â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 ⫱f2 ≘ f.
+ â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
/2 width=4 by frees_inv_bind_aux/ qed-.
fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀I,V,T. X = ⓕ[I]V.T →