(* SORT HIERARCHY ***********************************************************)
-(* sort hierarchy specifications *)
+(* sort hierarchy specification *)
record sh: Type[0] ≝ {
next: nat → nat; (* next sort in the hierarchy *)
next_lt: ∀k. k < next k (* strict monotonicity condition *)