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


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

Goals:
    A : Type  B : Type  f : A → B  l : list A  d : A  d' : B
  ============================
   (d' = f d → nth 0 (map f l) d' = f (nth 0 l d))

  
  A : Type
  B : Type
  f : A → B
  n : nat
  l : list A
  d : A
  d' : B
  IHn : ∀ l : list A, d' = f d → nth n (map f l) d' = f (nth n l d)
  ============================
   (d' = f d → nth (S n) (map f l) d' = f (nth (S n) l d))


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

Goals:
    A : Type  B : Type  f : A → B  d : A  d' : B
  ============================
   (d' = f d → nth 0 (map f []) d' = f (nth 0 [] d))

    A : Type  B : Type  f : A → B  a : A  l : list A  d : A  d' : B
  ============================
   (d' = f d → nth 0 (map f (a :: l)) d' = f (nth 0 (a :: l) d))

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

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


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l
DEBUG LTAC Evaluated term: l

Goals:
    A : Type  B : Type  f : A → B  d : A  d' : B
  ============================
   (d' = f d → d' = f d)

    A : Type  B : Type  f : A → B  a : A  l : list A  d : A  d' : B
  ============================
   (d' = f d → f a = f a)

  
  A : Type
  B : Type
  f : A → B
  n : nat
  d : A
  d' : B
  IHn : ∀ l : list A, d' = f d → nth n (map f l) d' = f (nth n l d)
  ============================
   (d' = f d → d' = f d)

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


DEBUG:Going to execute:
auto

Goals:
    A : Type  B : Type  f : A → B  d : A  d' : B
  ============================
   (d' = f d → d' = f d)

    A : Type  B : Type  f : A → B  a : A  l : list A  d : A  d' : B
  ============================
   (d' = f d → f a = f a)

  
  A : Type
  B : Type
  f : A → B
  n : nat
  d : A
  d' : B
  IHn : ∀ l : list A, d' = f d → nth n (map f l) d' = f (nth n l d)
  ============================
   (d' = f d → d' = f d)

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


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3