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


DEBUG:Going to execute:
congruence