update in ground_2 static_2 basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / web / static_2_src.tbl

diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
index 3793e689647562b50ef857abf3a0393cb060d1bd..07bc1856ad7d8a40923be17a05807fc793777d33 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
@@ -102,6 +102,10 @@ table {
    ]
    class "red"
    [ { "syntax" * } {
+        [ { "applicability condition" * } {
+             [ [ "properties" ] "ac" * ]
+          }
+        ]   
         [ { "equivalence up to exclusion binders" * } {
              [ [ "for lenvs" ] "lveq" + "( ? ≋ⓧ*[?,?] ? )" "lveq_length" + "lveq_lveq" * ]
           }
@@ -111,14 +115,10 @@ table {
              [ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ]
           }
         ]
-        [ { "head equivalence" * } {
+        [ { "sort-irrelevant head equivalence" * } {
              [ [ "for terms" ] "theq" + "( ? ⩳ ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ]
           }
         ]
-        [ { "tail sort-irrelevant equivalence" * } {
-             [ [ "" ] "tueq" + "( ? ≅ ? )" "tueq_tueq" * ]
-          }
-        ]
         [ { "sort-irrelevant equivalence" * } {
              [ [ "" ] "tdeq_ext" + "( ? ≛ ? )" + "( ? ⊢ ? ≛ ? )" * ]
              [ [ "" ] "tdeq" + "( ? ≛ ? )" "tdeq_tdeq" * ]