X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fweb%2Fbasic_2_src.tbl;h=1c4072923cbc73112a4e4321764e7115d66cc425;hb=5d669f492522b055f76c627eb89da97d0be05c2a;hp=4778311f7cd93f2ecb88bbaab8fb504f7f406291;hpb=63c047cae0056da7a69cb0740336d12259fbeb1a;p=helm.git

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 4778311f7..1c4072923 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
@@ -40,7 +40,7 @@ table {
         ]
 *)
         [ { "local env. ref. for stratified native validity" * } {
-             [ "lsubsv ( ? ⊢ ? ¡⫃[?,?] ? )" "lsubsv_lsubd" + "lsubsv_lsuba" + "lsubsv_lstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
+             [ "lsubsv ( ? ⊢ ? ¡⫃[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
           }
         ]
         [ { "stratified native validity" * } {
@@ -170,7 +170,7 @@ table {
           }
         ]
         [ { "iterated static type assignment" * } {
-             [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?,?] ? )" "lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?,?] ? )" "lstas_lift" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ]
+             [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_alt ( ⦃?,?⦄ ⊢ ? ••*[?,?] ? )" "lstas_lift" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ]
           }
         ]
      }
@@ -185,8 +185,12 @@ table {
              [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_sta" + "da_da" * ]
           }
         ]
-        [ { "stratified static type assignment" * } {
-             [ "sta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "sta_lift" + "sta_lpx_sn" + "sta_aaa" + "sta_sta" * ]
+        [ { "stratified equivalence" * } {
+             [ "steq ( ? ≡[?,?] ? )" "steq_steq" * ]
+          }
+        ]
+        [ { "static type assignment" * } {
+             [ "sta ( ⦃?,?⦄ ⊢ ? •[?] ? )" "sta_lift" + "sta_lpx_sn" + "sta_aaa" + "sta_sta" * ]
           }
         ]
         [ { "parameters" * } {