(* Advanced properties ******************************************************)
lemma frees_atom_drops: ∀b,L,i. ⬇*[b, 𝐔❴i❵] L ≘ ⋆ →
- â\88\80f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 â\86\91*[i]⫯f.
+ â\88\80f. ð\9d\90\88â¦\83fâ¦\84 â\86\92 L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 ⫯*[i]â\86\91f.
#b #L elim L -L /2 width=1 by frees_atom/
#L #I #IH *
[ #H lapply (drops_fwd_isid … H ?) -H // #H destruct
qed.
lemma frees_pair_drops: ∀f,K,V. K ⊢ 𝐅*⦃V⦄ ≘ f →
- â\88\80i,I,L. â¬\87*[i] L â\89\98 K.â\93\91{I}V â\86\92 L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 â\86\91*[i] ⫯f.
+ â\88\80i,I,L. â¬\87*[i] L â\89\98 K.â\93\91{I}V â\86\92 L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 ⫯*[i] â\86\91f.
#f #K #V #Hf #i elim i -i
[ #I #L #H lapply (drops_fwd_isid … H ?) -H /2 width=1 by frees_pair/
| #i #IH #I #L #H elim (drops_inv_succ … H) -H /3 width=2 by frees_lref/
qed.
lemma frees_unit_drops: ∀f. 𝐈⦃f⦄ → ∀I,K,i,L. ⬇*[i] L ≘ K.ⓤ{I} →
- L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 â\86\91*[i] ⫯f.
+ L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 ⫯*[i] â\86\91f.
#f #Hf #I #K #i elim i -i
[ #L #H lapply (drops_fwd_isid … H ?) -H /2 width=1 by frees_unit/
| #i #IH #Y #H elim (drops_inv_succ … H) -H
qed.
(*
lemma frees_sort_pushs: ∀f,K,s. K ⊢ 𝐅*⦃⋆s⦄ ≘ f →
- â\88\80i,L. â¬\87*[i] L â\89\98 K â\86\92 L â\8a¢ ð\9d\90\85*â¦\83â\8b\86sâ¦\84 â\89\98 â\86\91*[i] f.
+ â\88\80i,L. â¬\87*[i] L â\89\98 K â\86\92 L â\8a¢ ð\9d\90\85*â¦\83â\8b\86sâ¦\84 â\89\98 ⫯*[i] f.
#f #K #s #Hf #i elim i -i
[ #L #H lapply (drops_fwd_isid … H ?) -H //
| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_sort/
qed.
*)
lemma frees_lref_pushs: ∀f,K,j. K ⊢ 𝐅*⦃#j⦄ ≘ f →
- â\88\80i,L. â¬\87*[i] L â\89\98 K â\86\92 L â\8a¢ ð\9d\90\85*â¦\83#(i+j)â¦\84 â\89\98 â\86\91*[i] f.
+ â\88\80i,L. â¬\87*[i] L â\89\98 K â\86\92 L â\8a¢ ð\9d\90\85*â¦\83#(i+j)â¦\84 â\89\98 ⫯*[i] f.
#f #K #j #Hf #i elim i -i
[ #L #H lapply (drops_fwd_isid … H ?) -H //
| #i #IH #L #H elim (drops_inv_succ … H) -H
qed.
(*
lemma frees_gref_pushs: ∀f,K,l. K ⊢ 𝐅*⦃§l⦄ ≘ f →
- â\88\80i,L. â¬\87*[i] L â\89\98 K â\86\92 L â\8a¢ ð\9d\90\85*â¦\83§lâ¦\84 â\89\98 â\86\91*[i] f.
+ â\88\80i,L. â¬\87*[i] L â\89\98 K â\86\92 L â\8a¢ ð\9d\90\85*â¦\83§lâ¦\84 â\89\98 ⫯*[i] f.
#f #K #l #Hf #i elim i -i
[ #L #H lapply (drops_fwd_isid … H ?) -H //
| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_gref/
(* Advanced inversion lemmas ************************************************)
lemma frees_inv_lref_drops: ∀L,i,f. L ⊢ 𝐅*⦃#i⦄ ≘ f →
- â\88¨â\88¨ â\88\83â\88\83g. â¬\87*[â\92», ð\9d\90\94â\9d´iâ\9dµ] L â\89\98 â\8b\86 & ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91*[i] ⫯g
+ â\88¨â\88¨ â\88\83â\88\83g. â¬\87*[â\92», ð\9d\90\94â\9d´iâ\9dµ] L â\89\98 â\8b\86 & ð\9d\90\88â¦\83gâ¦\84 & f = ⫯*[i] â\86\91g
| ∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≘ g &
- â¬\87*[i] L â\89\98 K.â\93\91{I}V & f = â\86\91*[i] ⫯g
- | â\88\83â\88\83g,I,K. â¬\87*[i] L â\89\98 K.â\93¤{I} & ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91*[i] ⫯g.
+ â¬\87*[i] L â\89\98 K.â\93\91{I}V & f = ⫯*[i] â\86\91g
+ | â\88\83â\88\83g,I,K. â¬\87*[i] L â\89\98 K.â\93¤{I} & ð\9d\90\88â¦\83gâ¦\84 & f = ⫯*[i] â\86\91g.
#L elim L -L
[ #i #g | #L #I #IH * [ #g cases I -I [ #I | #I #V ] -IH | #i #g ] ] #H
[ elim (frees_inv_atom … H) -H #f #Hf #H destruct
qed-.
lemma frees_lifts_SO: ∀b,L,K. ⬇*[b, 𝐔❴1❵] L ≘ K → ∀T,U. ⬆*[1] T ≘ U →
- â\88\80f. K â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f â\86\92 L â\8a¢ ð\9d\90\85*â¦\83Uâ¦\84 â\89\98 â\86\91f.
+ â\88\80f. K â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f â\86\92 L â\8a¢ ð\9d\90\85*â¦\83Uâ¦\84 â\89\98 ⫯f.
#b #L #K #HLK #T #U #HTU #f #Hf
@(frees_lifts b … Hf … HTU) // (**) (* auto fails *)
qed.
/3 width=7 by frees_eq_repl_back, coafter_inj/
qed-.
-(* Note: this is used by lfxs_conf and might be modified *)
+(* Note: this is used by rex_conf and might be modified *)
lemma frees_inv_drops_next: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f1 →
∀I2,L2,V2,n. ⬇*[n] L1 ≘ L2.ⓑ{I2}V2 →
- â\88\80g1. ⫯g1 = ⫱*[n] f1 →
+ â\88\80g1. â\86\91g1 = ⫱*[n] f1 →
∃∃g2. L2 ⊢ 𝐅*⦃V2⦄ ≘ g2 & g2 ⊆ g1.
#f1 #L1 #T1 #H elim H -f1 -L1 -T1
[ #f1 #L1 #s #Hf1 #I2 #L2 #V2 #n #_ #g1 #H1 -I2 -L1 -s