X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fsh.ma;h=9e9b8adc173d9d572be15726499bf99b27b4c0d0;hp=8129473752d35bd95146f95897f66fe65431a75f;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma
index 812947375..9e9b8adc1 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma
@@ -12,18 +12,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/lib/arith.ma".
-include "static_2/notation/functions/upspoon_2.ma".
+include "ground/arith/nat.ma".
+include "static_2/notation/functions/uparrow_1_0.ma".
 
 (* SORT HIERARCHY ***********************************************************)
 
 (* sort hierarchy specification *)
 record sh: Type[0] ≝ {
-  next: nat → nat (* next sort in the hierarchy *)
+  sh_next: nat → nat (* next sort in the hierarchy *)
 }.
 
 interpretation "next sort (sort hierarchy)"
-   'UpSpoon h s = (next h s).
+   'UpArrow_1_0 h = (sh_next h).
 
 definition sh_is_next (h): relation nat ≝
-           λs1,s2. ⫯[h]s1 = s2.
+           λs1,s2. ⇡[h]s1 = s2.