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


DEBUG:Going to execute:
induction n in l, l', l'' |- *; destruct l; try intros [=<- <-]