| #p #I #V #T #HG #HL #HT destruct
elim (IH G L V) // #f1 #HV
elim (IH G (L.ⓑ[I]V) T) -IH // #f2 #HT
- elim (sor_isfin_ex f1 (⫱f2))
+ elim (sor_isfin_ex f1 (â«°f2))
/3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
| #I #V #T #HG #HL #HT destruct
elim (IH G L V) // #f1 #HV
theorem frees_bind_void:
∀f1,L,V. L ⊢ 𝐅+❪V❫ ≘ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅+❪T❫ ≘ f2 →
- â\88\80f. f1 â\8b\93 ⫱f2 ≘ f → ∀p,I. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f.
+ â\88\80f. f1 â\8b\93 â«°f2 ≘ f → ∀p,I. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f.
#f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
elim (frees_total (L.ⓑ[I]V) T) #f0 #Hf0
lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
lemma frees_inv_bind_void:
∀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§ â\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§ â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
#f #p #I #L #V #T #H
elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf
elim (frees_total (L.ⓧ) T) #f0 #Hf0
∀f,L,l. 𝐈❪f❫ → Q L (§l) f
) → (
∀f1,f2,f,p,I,L,V,T.
- L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 â\86\92 L.â\93§ â\8a¢ð\9d\90\85+â\9dªTâ\9d«â\89\98 f2 â\86\92 f1 â\8b\93 ⫱f2 ≘ f →
+ L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 â\86\92 L.â\93§ â\8a¢ð\9d\90\85+â\9dªTâ\9d«â\89\98 f2 â\86\92 f1 â\8b\93 â«°f2 ≘ f →
Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ[p,I]V.T) f
) → (
∀f1,f2,f,I,L,V,T.