- equivalene of tc_lfxs and lex + lfeq proved

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl

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 7737099cca0696a6e4a89522be7f945e33d0c6bc..c2bfdf8836ede786309b32e5b527d1e3151ed36b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -150,7 +150,7 @@ table {
    class "water"
    [ { "iterated static typing" * } {
         [ { "iterated extension on referred entries" * } {
-             [ [ "" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
+             [ [ "" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_lex" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
           }
         ]
      }
@@ -174,7 +174,7 @@ table {
           }
         ]
         [ { "syntactic equivalence on referred entries" * } {
-             [ [ "" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" * ]
+             [ [ "" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ]
           }
         ]
         [ { "generic extension on referred entries" * } {