From c2a67c225e01fc11b1ca479f45a159df2890bd8d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 11 Jun 2018 20:49:00 +0200 Subject: [PATCH] bug fix in basic_2 + cpcs_aaa_mono marked as lemma 1500 + fix in basic_2 web page --- .../contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma | 1 + matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma index a1361c2f0..13d12e5ad 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma @@ -19,6 +19,7 @@ include "basic_2/rt_equivalence/cpcs_cprs.ma". (* Main inversion lemmas with atomic arity assignment on terms **************) +(* Note: lemma 1500 *) theorem cpcs_aaa_mono (h) (G) (L): ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → A1 = A2. 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 413cf84ab..0ddb5a0b2 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 @@ -37,7 +37,7 @@ table { (* [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ] *) - [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "nv_drops" "nv_fqus" + "nv_aaa" + "snv_fsb" (* + "snv_lpr" + "snv_scpes" + "snv_preserve" *) * ] + [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "nv_drops" + "nv_fqus" + "nv_aaa" + "nv_fsb" (* + "snv_lpr" + "snv_scpes" + "snv_preserve" *) * ] } ] } -- 2.39.2