data Nat = Z | S Nat
     deriving (Eq, Show)

double :: Nat -> Nat
double x = case x of
       Z -> Z
       S x' -> S ( S ( double x' ) )

data List a = Nil | Cons a (List a)
    deriving (Eq, Show)

doubles :: List Nat -> List Nat
doubles xs = case xs of
  Nil -> Nil
  Cons x xss -> Cons ( double x ) ( doubles xss )

t1 = doubles $ Cons (S Z) ( Cons (S (S Z )) Nil)

append :: List a -> List a -> List a
append xs ys = case xs of
  Nil        -> ys
  Cons x xss -> Cons x (append xss ys)

t2 = append ( Cons Z ( Cons (S (S Z )) Nil)) (Cons Z Nil)
t3 = append ( Cons 1 ( Cons 2 Nil)) (Cons 3 Nil)

len :: List a -> Nat
len xs = case xs of
    Nil        -> Z
    Cons x xss -> S ( len xss )

t4 = len $ append ( Cons Z ( Cons (S (S Z )) Nil)) (Cons Z Nil)
t5 = len $ doubles $ append ( Cons Z ( Cons (S (S Z )) Nil)) (Cons Z Nil)
t6 = t4 == t5