(VAR
  x : a
  y : a
  xs : alist
  f : a -> a
  g : a -> a
)
(FUN
  nil : alist
  cons : a -> alist -> alist
  map : (a -> a) -> alist -> alist
)
(RULES
  map (\x. f x) nil -> nil,
  map (\x. f x) (cons x xs) -> cons (f x) (map (\x. f x) xs),
  map (\x. f x) (map (\x. g x) xs) -> map (\y. f (g y)) xs
)