Operationen auf Listen (I)

data List a = Nil | Cons a (List a)

• append xs ys = case xs of
       Nil        -> 
       Cons x xs' ->
  

• Übung: formuliere und beweise: append ist assoziativ.

• reverse xs = case xs of
       Nil        -> 
       Cons x xs' ->
  

• beweise:

  forall xs . reverse (reverse xs) == xs