data List = Nil unit | Cons nat * List in
fun isempty : List -> nat =
  \ natlist : List ->
        (case (exposeList natlist) of
           empty -> S Z
         | not -> Z)
in (isempty (Nil unit))