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


DEBUG:Going to execute:
induction n in l, l', l'' |- *

Goals:
    A : Type  B : Type  f : A → B  l : list A  l' : list A  l'' : list A
  ============================
   (chop 0 l = (l', l'') → chop 0 (map f l) = (map f l', map f l''))

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


DEBUG:Going to execute:
destruct l
DEBUG LTAC Evaluated term: n

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

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

  
  A : Type
  B : Type
  f : A → B
  n : nat
  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) [] = (l', l'') → chop (S n) (map f []) = (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'')
  ============================
   (chop (S n) (a :: l) = (l', l'')
    → chop (S n) (map f (a :: l)) = (map f l', map f l''))


DEBUG:Going to execute:
try intros [=<- <-]
DEBUG LTAC Evaluated term: l
DEBUG LTAC Evaluated term: l