X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fexamples%2Fex_cnv_eta.ma;h=1eb9cd38b800102d0d6b990bf6af4384fd2c42a6;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hp=2b3dfcd4c5c9e7f9468929341ae8595c4de7442a;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma index 2b3dfcd4c..1eb9cd38b 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma @@ -17,10 +17,11 @@ include "basic_2/dynamic/cnv.ma". (* EXAMPLES *****************************************************************) -(* Extended validy (basic_2B) vs. restricted validity (basic_1A) ************) +(* Extended validy (λδ-2A) vs. restricted validity (λδ-1B) ******************) (* Note: extended validity of a closure, height of cnv_appl > 1 *) -lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 !*[h]. +lemma cnv_extended (h) (p) (G) (L): + ∀s. ❪G,L.ⓛ⋆s.ⓛⓛ[p]⋆s.⋆s.ⓛ#0❫ ⊢ ⓐ#2.#0 ![h,𝛚]. #h #p #G #L #s @(cnv_appl … 2 p … (⋆s) … (⋆s)) [ // @@ -32,15 +33,16 @@ lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0 qed. (* Note: restricted validity of the η-expanded closure, height of cnv_appl = 1 **) -lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![h]. +lemma cnv_restricted (h) (p) (G) (L): + ∀s. ❪G,L.ⓛ⋆s.ⓛⓛ[p]⋆s.⋆s.ⓛⓛ[p]⋆s.ⓐ#0.#1❫ ⊢ ⓐ#2.#0 ![h,𝟐]. #h #p #G #L #s @(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2)) -[ /2 width=1 by ylt_inj/ +[ // | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/ | @cnv_zero @cnv_bind // @(cnv_appl … 1 p … (⋆s) … (⋆s)) - [ /2 width=1 by ylt_inj/ + [ // | /2 width=1 by cnv_sort, cnv_zero/ | /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/ | /2 width=3 by cpms_ell, lifts_sort/