Goal:
  
  A : Type
  B : Type
  f : A → B
  n : nat
  l' : list A
  l'' : list A
  IHn : ∀ l l' l'' : list A,
          chop n l = (l', l'') → chop n (map f l) = (map f l', map f l'')
  ============================
   (chop (S n) [] = (l', l'') → chop (S n) (map f []) = (map f l', map f l''))


DEBUG:Going to execute:
intros [=<- <-]