Goal:
  
  A : Type
  B : Type
  n : nat
  f : A → B
  IHn : ∀ l : list A, firstn n (map f l) = map f (firstn n l)
  ============================
   (∀ l : list A, firstn (S n) (map f l) = map f (firstn (S n) l))


DEBUG:Going to execute:
destruct l

Goals:
  
  A : Type
  B : Type
  n : nat
  f : A → B
  IHn : ∀ l : list A, firstn n (map f l) = map f (firstn n l)
  ============================
   (firstn (S n) (map f []) = map f (firstn (S n) []))

  
  A : Type
  B : Type
  n : nat
  f : A → B
  IHn : ∀ l : list A, firstn n (map f l) = map f (firstn n l)
  a : A
  l : list A
  ============================
   (firstn (S n) (map f (a :: l)) = map f (firstn (S n) (a :: l)))


DEBUG:Going to execute:
simpl in *

Goals:
  
  A : Type
  B : Type
  n : nat
  f : A → B
  IHn : ∀ l : list A, firstn n (map f l) = map f (firstn n l)
  ============================
   ([] = [])

  
  A : Type
  B : Type
  n : nat
  f : A → B
  IHn : ∀ l : list A, firstn n (map f l) = map f (firstn n l)
  a : A
  l : list A
  ============================
   (f a :: firstn n (map f l) = f a :: map f (firstn n l))


DEBUG:Going to execute:
congruence

Goals:
  
  A : Type
  B : Type
  n : nat
  f : A → B
  IHn : ∀ l : list A, firstn n (map f l) = map f (firstn n l)
  ============================
   ([] = [])

  
  A : Type
  B : Type
  n : nat
  f : A → B
  IHn : ∀ l : list A, firstn n (map f l) = map f (firstn n l)
  a : A
  l : list A
  ============================
   (f a :: firstn n (map f l) = f a :: map f (firstn n l))


DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1