(* SORT HIERARCHY ***********************************************************)
(* sort hierarchy specification *)
record sh: Type[0] ≝ {
(* SORT HIERARCHY ***********************************************************)
(* sort hierarchy specification *)
record sh: Type[0] ≝ {