Goal:
    A : Type  B : Type  f : A → B  a : A  n : nat
  ============================
   (map f (repeat a n) = repeat (f a) n)


DEBUG:Going to execute:
induction n

Goals:
    A : Type  B : Type  f : A → B  a : A
  ============================
   (map f (repeat a 0) = repeat (f a) 0)

  
  A : Type
  B : Type
  f : A → B
  a : A
  n : nat
  IHn : map f (repeat a n) = repeat (f a) n
  ============================
   (map f (repeat a (S n)) = repeat (f a) (S n))


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: n

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

  
  A : Type
  B : Type
  f : A → B
  a : A
  n : nat
  IHn : map f (repeat a n) = repeat (f a) n
  ============================
   (f a :: map f (repeat a n) = f a :: repeat (f a) n)


DEBUG:Going to execute:
congruence

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

  
  A : Type
  B : Type
  f : A → B
  a : A
  n : nat
  IHn : map f (repeat a n) = repeat (f a) n
  ============================
   (f a :: map f (repeat a n) = f a :: repeat (f a) n)


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