From cce6d001d2c71a0a7f4b6d4bb136d105224b2cd1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 14 May 2018 20:49:03 +0200 Subject: [PATCH] update in basic_2 + advances on native validity --- .../lambdadelta/basic_2/dynamic/nv_drops.ma | 132 ++++++++++++++++++ .../lambdadelta/basic_2/dynamic/nv_fqus.ma | 36 +++++ .../lambdadelta/basic_2/dynamic/partial.txt | 2 +- .../lambdadelta/basic_2/dynamic/snv_lift.ma | 124 ---------------- .../basic_2/rt_computation/cpms_drops.ma | 16 ++- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 6 files changed, 183 insertions(+), 129 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fqus.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_drops.ma new file mode 100644 index 000000000..9d32d0345 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_drops.ma @@ -0,0 +1,132 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_computation/cpms_drops.ma". +include "basic_2/dynamic/nv.ma". + +(* NATIVE VALIDITY FOR TERMS ************************************************) + +(* Advanced dproperties *****************************************************) + +(* Basic_2A1: uses: snv_lref *) +lemma nv_lref_drops (a) (h) (G): ∀I,K,V,i,L. ⦃G, K⦄ ⊢ V ![a, h] → + ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G, L⦄ ⊢ #i ![a, h]. +#a #h #G #I #K #V #i elim i -i +[ #L #HV #H + lapply (drops_fwd_isid … H ?) -H // #H destruct + /2 width=1 by nv_zero/ +| #i #IH #L #HV #H + elim (drops_inv_succ … H) -H #J0 #K0 #HK0 #H destruct + /3 width=1 by nv_lref/ +] +qed. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_2A1: uses: snv_inv_lref *) +lemma nv_inv_lref_drops (a) (h) (G): + ∀i,L. ⦃G, L⦄ ⊢ #i ![a, h] → + ∃∃I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ![a, h]. +#a #h #G #i elim i -i +[ #L #H + elim (nv_inv_zero … H) -H #I #K #V #HV #H destruct + /3 width=5 by drops_refl, ex2_3_intro/ +| #i #IH #X #H + elim (nv_inv_lref … H) -H #I #L #HL #H destruct + elim (IH … HL) -IH -HL #J #K #V #HLK #HV + /3 width=5 by drops_drop, ex2_3_intro/ +] +qed-. + +(* Properties with generic slicing for local environments *******************) + +(* Basic_2A1: uses: snv_lift *) +lemma sv_lifts (a) (h): ∀G. d_liftable1 (nv a h G). +#a #h #G #K #T +@(fqup_wf_ind_eq (Ⓣ) … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * * [|||| * ] +[ #s #HG #HK #HT #_ #b #f #L #_ #X #H2 destruct + >(lifts_inv_sort1 … H2) -X -K -f // +| #i #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct + elim (nv_inv_lref_drops … H1) -H1 #I0 #K0 #V #HK0 #HV + elim (lifts_inv_lref1 … H2) -H2 #j #Hf #H destruct +(**) (* this should be a lemma *) + lapply (drops_trans … HLK … HK0 ??) -HLK [3,6: |*: // ] #H + elim (drops_split_trans … H) -H [1,6: |*: /2 width=6 by after_uni_dx/ ] #Y #HL #HY + lapply (drops_tls_at … Hf … HY) -HY #HY + elim (drops_inv_skip2 … HY) -HY #Z #L0 #HLK0 #HZ #H destruct + elim (liftsb_inv_pair_sn … HZ) -HZ #W #HVW #H destruct +(**) (* end of the lemma *) + /4 width=8 by nv_lref_drops, fqup_lref, drops_inv_gen/ +| #l #HG #HK #HT #H1 #b #f #L #_ #X #_ destruct + elim (nv_inv_gref … H1) +| #p #I #V #T #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct + elim (nv_inv_bind … H1) -H1 #HV #HT + elim (lifts_inv_bind1 … H2) -H2 #W #U #HVW #HTU #H destruct + /5 width=8 by nv_bind, drops_skip, ext2_pair/ +| #V #T #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct + elim (nv_inv_appl … H1) #n #p #W0 #U0 #Ha #HV #HT #HVW0 #HTW0 + elim (lifts_inv_flat1 … H2) -H2 #W #U #HVW #HTU #H destruct + elim (lifts_total W0 f) + elim (lifts_total U0 (⫯f)) + /4 width=17 by nv_appl, cpms_lifts_bi, lifts_bind/ +| #V #T #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct + elim (nv_inv_cast … H1) #U0 #HV #HT #HVU0 #HTU0 + elim (lifts_inv_flat1 … H2) -H2 #W #U #HVW #HTU #H destruct + elim (lifts_total U0 f) + /3 width=12 by nv_cast, cpms_lifts_bi/ +] +qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: uses: snv_inv_lift *) +lemma nv_inv_lifts (a) (h): ∀G. d_deliftable1 (nv a h G). +#a #h #G #L #U +@(fqup_wf_ind_eq (Ⓣ) … G L U) -G -L -U #G0 #L0 #U0 #IH #G #L * * [|||| * ] +[ #s #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct + >(lifts_inv_sort2 … H2) -X -L -f // +| #j #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct + elim (nv_inv_lref_drops … H1) -H1 #I0 #L0 #W #HL0 #HW + elim (lifts_inv_lref2 … H2) -H2 #i #Hf #H destruct +(**) (* this should be a lemma *) + lapply (drops_split_div … HLK (𝐔❴i❵) ???) -HLK [4,8: * |*: // ] #Y0 #HK #HLY0 + lapply (drops_conf … HL0 … HLY0 ??) -HLY0 [3,6: |*: /2 width=6 by after_uni_dx/ ] #HLY0 + lapply (drops_tls_at … Hf … HLY0) -HLY0 #HLY0 + elim (drops_inv_skip1 … HLY0) -HLY0 #Z #K0 #HLK0 #HZ #H destruct + elim (liftsb_inv_pair_dx … HZ) -HZ #V #HVW #H destruct +(**) (* end of the lemma *) + /4 width=8 by nv_lref_drops, fqup_lref, drops_inv_F/ +| #l #HG #HL #HU #H1 #b #f #K #_ #X #_ destruct + elim (nv_inv_gref … H1) +| #p #I #W #U #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct + elim (nv_inv_bind … H1) -H1 #HW #HU + elim (lifts_inv_bind2 … H2) -H2 #V #T #HVW #HTU #H destruct + /5 width=8 by nv_bind, drops_skip, ext2_pair/ +| #W #U #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct + elim (nv_inv_appl … H1) #n #p #W0 #U0 #Ha #HW #HU #HW0 #HU0 + elim (lifts_inv_flat2 … H2) -H2 #V #T #HVW #HTU #H destruct + elim (cpms_inv_lifts_sn … HW0 … HLK … HVW) -HW0 #V0 #HVW0 #HV0 + elim (cpms_inv_lifts_sn … HU0 … HLK … HTU) -HU0 #X0 #H #HT0 + elim (lifts_inv_bind2 … H) -H #X #T0 #HX #HTU0 #H destruct + lapply (lifts_inj … HX … HVW0) -HX #H destruct + /3 width=8 by nv_appl/ +| #W #U #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct + elim (nv_inv_cast … H1) #U0 #HW #HU #HWU0 #HU0 + elim (lifts_inv_flat2 … H2) -H2 #V #T #HVW #HTU #H destruct + elim (cpms_inv_lifts_sn … HWU0 … HLK … HVW) -HWU0 #V0 #HVU0 #HV0 + elim (cpms_inv_lifts_sn … HU0 … HLK … HTU) -HU0 #X #HX #HTV0 + lapply (lifts_inj … HX … HVU0) -HX #H destruct + /3 width=8 by nv_cast/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fqus.ma new file mode 100644 index 000000000..f0649de3e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nv_fqus.ma @@ -0,0 +1,36 @@ +(* Properties on subclosure *************************************************) + +lemma snv_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I1 #G1 #L1 #V1 #H + elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2 + lapply (drop_inv_O2 … H) -H #H destruct // +|2: * +|5,6: /3 width=8 by snv_inv_lift/ +] +[1,3: #a #I #G1 #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H // +|2,4: * #G1 #L1 #V1 #T1 #H + [1,3: elim (snv_inv_appl … H) -H // + |2,4: elim (snv_inv_cast … H) -H // + ] +] +qed-. + +lemma snv_fquq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fquq_inv_gen … H) -H [|*] +/2 width=5 by snv_fqu_conf/ +qed-. + +lemma snv_fqup_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +/3 width=5 by fqup_strap1, snv_fqu_conf/ +qed-. + +lemma snv_fqus_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_gen … H) -H [|*] +/2 width=5 by snv_fqup_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt index f8e181d78..e5b27fe2d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt @@ -1 +1 @@ -nv.ma +nv.ma nv_drops.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma deleted file mode 100644 index 6430cbcd5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma +++ /dev/null @@ -1,124 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/multiple/fqus_alt.ma". -include "basic_2/computation/scpds_lift.ma". -include "basic_2/dynamic/snv.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Relocation properties ****************************************************) - -| nv_lref: ∀I,G,L,K,V,i. ⬇[i] L ≘ K.ⓑ{I}V → nv a h G K V → nv a h G L (#i) - -lemma nv_inv_lref: ∀a,h,G,L,i. ⦃G, L⦄ ⊢ #i ![a, h] → - ∃∃I,K,V. ⬇[i] L ≘ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ![a, h]. -/2 width=3 by nv_inv_lref_aux/ qed-. - - -lemma snv_lift: ∀h,o,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, o] → ∀L,b,l,k. ⬇[b, l, k] L ≘ K → - ∀U. ⬆[l, k] T ≘ U → ⦃G, L⦄ ⊢ U ¡[h, o]. -#h #o #G #K #T #H elim H -G -K -T -[ #G #K #s #L #b #l #k #_ #X #H - >(lift_inv_sort1 … H) -X -K -l -k // -| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #b #l #k #HLK #X #H - elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (drop_trans_le … HLK … HK0) -K /2 width=2 by ylt_fwd_le/ #X #HL0 #H - elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #L0 #W #HLK0 #HVW #H destruct - /3 width=9 by snv_lref/ - | lapply (drop_trans_ge … HLK … HK0 ?) -K - /3 width=9 by snv_lref, drop_inv_gen/ - ] -| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #b #l #k #HLK #X #H - elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct - /4 width=5 by snv_bind, drop_skip/ -| #a #G #K #V #W0 #T #U0 #d #_ #_ #HVW0 #HTU0 #IHV #IHT #L #b #l #k #HLK #X #H - elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct - elim (lift_total W0 l k) - elim (lift_total U0 (l+1) k) - /4 width=17 by snv_appl, scpds_lift, lift_bind/ -| #G #K #V #T #U0 #_ #_ #HVU0 #HTU0 #IHV #IHT #L #b #l #k #HLK #X #H - elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct - elim (lift_total U0 l k) - /3 width=12 by snv_cast, scpds_lift/ -] -qed. - -lemma snv_inv_lift: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, o] → ∀K,b,l,k. ⬇[b, l, k] L ≘ K → - ∀T. ⬆[l, k] T ≘ U → ⦃G, K⦄ ⊢ T ¡[h, o]. -#h #o #G #L #U #H elim H -G -L -U -[ #G #L #s #K #b #l #k #_ #X #H - >(lift_inv_sort2 … H) -X -L -l -k // -| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #b #l #k #HLK #X #H - elim (lift_inv_lref2 … H) * #Hil #H destruct - [ elim (drop_conf_le … HLK … HL0) -L /2 width=2 by ylt_fwd_le/ #X #HK0 #H - elim (drop_inv_skip1 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K0 #V #HLK0 #HVW #H destruct - /3 width=12 by snv_lref/ - | lapply (drop_conf_ge … HLK … HL0 ?) -L /3 width=9 by snv_lref/ - ] -| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #b #l #k #HLK #X #H - elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct - /4 width=5 by snv_bind, drop_skip/ -| #a #G #L #W #W1 #U #U1 #d #_ #_ #HW1 #HU1 #IHW #IHU #K #b #l #k #HLK #X #H - elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct - elim (scpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0 - elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU0 - elim (lift_inv_bind2 … H) -H #Y #U0 #HY #HU01 #H destruct - lapply (lift_inj … HY … HW01) -HY #H destruct - /3 width=6 by snv_appl/ -| #G #L #W #U #U1 #_ #_ #HWU1 #HU1 #IHW #IHU #K #b #l #k #HLK #X #H - elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct - elim (scpds_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0 - elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #HX #HTU0 - lapply (lift_inj … HX … HU01) -HX #H destruct - /3 width=5 by snv_cast/ -] -qed-. - -(* Properties on subclosure *************************************************) - -lemma snv_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I1 #G1 #L1 #V1 #H - elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2 - lapply (drop_inv_O2 … H) -H #H destruct // -|2: * -|5,6: /3 width=8 by snv_inv_lift/ -] -[1,3: #a #I #G1 #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H // -|2,4: * #G1 #L1 #V1 #T1 #H - [1,3: elim (snv_inv_appl … H) -H // - |2,4: elim (snv_inv_cast … H) -H // - ] -] -qed-. - -lemma snv_fquq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fquq_inv_gen … H) -H [|*] -/2 width=5 by snv_fqu_conf/ -qed-. - -lemma snv_fqup_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -/3 width=5 by fqup_strap1, snv_fqu_conf/ -qed-. - -lemma snv_fqus_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o]. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_gen … H) -H [|*] -/2 width=5 by snv_fqup_conf/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma index b719f52b5..568100b54 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.ma @@ -63,15 +63,20 @@ lemma cpms_inv_lref1_drops (n) (h) (G): /4 width=8 by cpms_step_dx, ex4_4_intro, or3_intro2/ ] ] -qed-. +qed-. (* Properties with generic slicing for local environments *******************) +lemma cpms_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpms h G L n). +/3 width=6 by d2_liftable_sn_ltc, cpm_lifts_sn/ qed-. + (* Basic_2A1: uses: scpds_lift *) (* Basic_2A1: includes: cprs_lift *) (* Basic_1: includes: pr3_lift *) -lemma cpms_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpms h G L n). -/3 width=6 by d2_liftable_sn_ltc, cpm_lifts_sn/ qed-. +lemma cpms_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpms h G L n). +#n #h #G @d_liftable2_sn_bi +/2 width=6 by cpms_lifts_sn, lifts_mono/ +qed-. (* Inversion lemmas with generic slicing for local environments *************) @@ -80,3 +85,8 @@ lemma cpms_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpms h G L n). (* Basic_1: includes: pr3_gen_lift *) lemma cpms_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpms h G L n). /3 width=6 by d2_deliftable_sn_ltc, cpm_inv_lifts_sn/ qed-. + +lemma cpms_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpms h G L n). +#n #h #G @d_deliftable2_sn_bi +/2 width=6 by cpms_inv_lifts_sn, lifts_inj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index e5ec82baf..6cf0a3dac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -39,7 +39,7 @@ table { (* [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ] *) - [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" (* "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" *) * ] + [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "nv_drops" (* + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" *) * ] } ] } -- 2.39.2