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'')
  ============================
   (chop (S n) (a :: l) = (l', l'')
    → chop (S n) (map f (a :: l)) = (map f l', map f l''))


DEBUG:Going to execute:
intros [=<- <-]

Goals:
    A : Type  B : Type  f : A → B
  ============================
   (chop 0 (map f []) = (map f [], map f []))

    A : Type  B : Type  f : A → B  a : A  l : list A
  ============================
   (chop 0 (map f (a :: l)) = (map f [], map f (a :: l)))

  
  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'')
  ============================
   (chop (S n) (map f []) = (map f [], map f []))

  
  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'')
  ============================
   (chop (S n) (a :: l) = (l', l'')
    → chop (S n) (map f (a :: l)) = (map f l', map f l''))


DEBUG:Going to execute:
simpl
Level 0: Backtrace:

Unexpected introduction pattern (at most 1 was expected in the branch).

Goals:
    A : Type  B : Type  f : A → B
  ============================
   (([], []) = ([], []))

    A : Type  B : Type  f : A → B  a : A  l : list A
  ============================
   (([], f a :: map f l) = ([], f a :: map f l))

  
  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'')
  ============================
   (([], []) = ([], []))

  
  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:
try congruence