Goal:
    A : Type  B : Type  f : A → B  n : nat  l : list A  d : A  d' : B
  ============================
   (d' = f d → nth n (map f l) d' = f (nth n l d))


DEBUG:Going to execute:
induction n in l |- *; destruct l