Goal:
  
  A : Type
  B : Type
  f : A → B
  n : nat
  a : A
  l : list A
  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'')
  ============================
   ((let '(l, r) := chop n l in (a :: l, r)) = (l', l'')
    → (let '(l, r) := chop n (map f l) in (f a :: l, r)) =
      (map f l', map f l''))


DEBUG:Going to execute:
congruence