Goal:
  
  A : Type
  size : A → nat
  l : list A
  f : A → A
  H : ∀ x : A, size x = size (f x)
  ============================
   (list_size size (map f l) = list_size size l)


DEBUG:Going to execute:
induction l; simpl