X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_drops.ma;h=aa4f34998ffe6732e4d870dec140ff248daaf5ff;hb=926796df5884453d8f0cf9f294d7776d469ef45b;hp=fd4ec0ce18854cdcac109112a786ab1ddd8db7d0;hpb=e06774421eb3b8f4438a6876cc1ab4262ef16f6e;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma index fd4ec0ce1..aa4f34998 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma @@ -14,19 +14,19 @@ include "ground_2/relocation/rtmap_pushs.ma". include "ground_2/relocation/rtmap_coafter.ma". -include "basic_2/relocation/lifts_lifts.ma". -include "basic_2/relocation/drops.ma". +include "basic_2/relocation/drops_drops.ma". include "basic_2/static/frees.ma". (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) (* Advanced properties ******************************************************) -lemma frees_lref_atom: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ → L ⊢ 𝐅*⦃#i⦄ ≡ 𝐈𝐝. -#L elim L -L /2 width=1 by frees_atom/ +lemma frees_lref_atom: ∀b,L,i. ⬇*[b, 𝐔❴i❵] L ≡ ⋆ → + ∀f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃#i⦄ ≡ f. +#b #L elim L -L /2 width=1 by frees_atom/ #L #I #V #IH * [ #H lapply (drops_fwd_isid … H ?) -H // #H destruct -| /4 width=3 by frees_lref, drops_inv_drop1/ +| /5 width=3 by frees_eq_repl_back, frees_lref, drops_inv_drop1, eq_push_inv_isid/ ] qed. @@ -58,6 +58,91 @@ qed-. (* Properties with generic slicing for local environments *******************) +axiom coafter_inv_xpx: ∀g2,f1,g. g2 ~⊚ ↑f1 ≡ g → ∀n. @⦃0, g2⦄ ≡ n → + ∃∃f2,f. f2 ~⊚ f1 ≡ f & ⫱*[n]g2 = ↑f2 & ⫱*[n]g = ↑f. +(* +#g2 #g1 #g #Hg #n #Hg2 +lapply (coafter_tls … Hg2 … Hg) -Hg #Hg +lapply (at_pxx_tls … Hg2) -Hg2 #H +elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2 +elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0 destruct +