Goal:
  
  A : Type
  B : Type
  n : nat
  f : A → B
  IHn : ∀ l : list A, firstn n (map f l) = map f (firstn n l)
  ============================
   (∀ l : list A, firstn (S n) (map f l) = map f (firstn (S n) l))


DEBUG:Going to execute:
destruct l; simpl in *