(* *)
(**************************************************************************)
-include "ground_2/lib/arith.ma".
+include "ground/lib/arith.ma".
include "static_2/notation/functions/upspoon_2.ma".
(* SORT HIERARCHY ***********************************************************)
interpretation "next sort (sort hierarchy)"
'UpSpoon h s = (next h s).
+
+definition sh_is_next (h): relation nat ≝
+ λs1,s2. ⫯[h]s1 = s2.