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)
  ============================
   ((let '(l, r) := chop n (map f l) in (f a :: l, r)) =
    (map f (a :: l0), map f l1))


DEBUG:Going to execute:
rewrite IHn
DEBUG LTAC Evaluated term: (IHn l l0 l1 Heq)