Goal:
  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  l : list C
  l' : list D
  ============================
   (∀ n : nat,
      mapi_rec f (map2 g l l') n =
      map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n l l')


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

Goals:
  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  l' : list D
  ============================
   (∀ n : nat,
      mapi_rec f (map2 g [] l') n =
      map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n [] l')

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  a : C
  l : list C
  l' : list D
  IHl : ∀ (l' : list D) (n : nat),
          mapi_rec f (map2 g l l') n =
          map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n l l'
  ============================
   (∀ n : nat,
      mapi_rec f (map2 g (a :: l) l') n =
      map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n (a :: l) l')


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

Goals:
  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  l' : list D
  n : nat
  ============================
   (mapi_rec f (map2 g [] l') n =
    map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n [] l')

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  a : C
  l : list C
  l' : list D
  IHl : ∀ (l' : list D) (n : nat),
          mapi_rec f (map2 g l l') n =
          map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n l l'
  n : nat
  ============================
   (mapi_rec f (map2 g (a :: l) l') n =
    map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n (a :: l) l')


DEBUG:Going to execute:
destruct l'

Goals:
  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  n : nat
  ============================
   (mapi_rec f (map2 g [] []) n =
    map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n [] [])

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  d : D
  l' : list D
  n : nat
  ============================
   (mapi_rec f (map2 g [] (d :: l')) n =
    map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n [] (d :: l'))

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  a : C
  l : list C
  IHl : ∀ (l' : list D) (n : nat),
          mapi_rec f (map2 g l l') n =
          map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n l l'
  n : nat
  ============================
   (mapi_rec f (map2 g (a :: l) []) n =
    map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n (a :: l) [])

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  a : C
  l : list C
  d : D
  l' : list D
  IHl : ∀ (l' : list D) (n : nat),
          mapi_rec f (map2 g l l') n =
          map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n l l'
  n : nat
  ============================
   (mapi_rec f (map2 g (a :: l) (d :: l')) n =
    map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n (a :: l) (d :: l'))


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

Goals:
  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  n : nat
  ============================
   ([] = [])

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  d : D
  l' : list D
  n : nat
  ============================
   ([] = [])

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  a : C
  l : list C
  IHl : ∀ (l' : list D) (n : nat),
          mapi_rec f (map2 g l l') n =
          map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n l l'
  n : nat
  ============================
   ([] = [])

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  a : C
  l : list C
  d : D
  l' : list D
  IHl : ∀ (l' : list D) (n : nat),
          mapi_rec f (map2 g l l') n =
          map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n l l'
  n : nat
  ============================
   (f n (g a d) :: mapi_rec f (map2 g l l') (S n) =
    f n (g a d)
    :: map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) (S n) l l')


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  n : nat
  ============================
   ([] = [])

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  d : D
  l' : list D
  n : nat
  ============================
   ([] = [])

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  a : C
  l : list C
  IHl : ∀ (l' : list D) (n : nat),
          mapi_rec f (map2 g l l') n =
          map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n l l'
  n : nat
  ============================
   ([] = [])

  
  A : Type
  B : Type
  C : Type
  D : Type
  f : nat → A → B
  g : C → D → A
  a : C
  l : list C
  d : D
  l' : list D
  IHl : ∀ (l' : list D) (n : nat),
          mapi_rec f (map2 g l l') n =
          map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) n l l'
  n : nat
  ============================
   (f n (g a d) :: mapi_rec f (map2 g l l') (S n) =
    f n (g a d)
    :: map2i_rec (λ (i : nat) (x : C) (y : D), f i (g x y)) (S n) l l')


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