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'')
  l0 : list A
  l1 : list A
  Heq : chop n l = (l0, l1)
  ============================
   ((a :: l0, l1) = (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:
<coq-core.plugins.ltac::specialize@0> $1
Level 0: Backtrace:

Tactic failure: congruence failed.
Level 0: Backtrace:

Tactic failure: congruence failed.
DEBUG LTAC Evaluated term: (chop n l)