foo : Nat -> String
foo n = case n of
          0 => "z"
          S _ => "s"
bar : Nat -> String -> String
bar x y = case x of
            0 => y
            S _ => y ++ y
append : List a -> List a -> List a
append xs ys = case xs of
                 [] => ys
                 x :: xs => x :: append xs ys