succ (successor)
successor of this element in an enumerated type
letting D be new type enum { North, East, South, West }
find a : D such that a = succ(South) $West
This result West
shows a
must be the successor of South
.
See it demonstrated here.