]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
update in static_2 and basic_2 for the article
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / web / static_2_src.tbl
index 44690009a001fb7a21d36fd2fc90c2dea41b5c21..62716221841a87d0c7227907d1772cfa3538c831 100644 (file)
@@ -86,7 +86,7 @@ table {
         [ { "generic and uniform relocation" * } {
              [ [ "for binders" ] "lifts_bind" + "( ⇧*[?] ? ≘ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ]
              [ [ "for term vectors" ] "lifts_vector" + "( ⇧*[?] ? ≘ ? )" "lifts_lifts_vector" * ]
-             [ [ "for terms" ] "lifts" + "( ⇧*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_tweq" + "lifts_toeq" + "lifts_lifts" * ]
+             [ [ "for terms" ] "lifts" + "( ⇧*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_tweq" + "lifts_teqo" + "lifts_lifts" * ]
           }
         ]
         [ { "syntactic equivalence" * } {
@@ -117,7 +117,7 @@ table {
           }
         ]
         [ { "sort-irrelevant outer equivalence" * } {
-             [ [ "for terms" ] "toeq" + "( ? ⩳ ? )" "toeq_simple" + "toeq_tdeq" + "toeq_toeq" + "toeq_simple_vector" * ]
+             [ [ "for terms" ] "teqo" + "( ? ⩳ ? )" "teqo_simple" + "teqo_tdeq" + "teqo_teqo" + "teqo_simple_vector" * ]
           }
         ]
         [ { "sort-irrelevant whd equivalence" * } {