Goal:
  
  A : Type
  B : Type
  f : A → B
  n : nat
  a : A
  l : list A
  l0 : list A
  l1 : list A
  IHn : chop n (map f l) = (map f l0, map f l1)
  Heq : chop n l = (l0, l1)
  ============================
   ((f a :: map f l0, map f l1) = (map f (a :: l0), map f l1))


DEBUG:Going to execute:
solve
[ trivial
with eq_true
| reflexivity
| symmetry; trivial
| contradiction
| congruence ]