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


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

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

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


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

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

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


DEBUG:Going to execute:
destruct l'

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

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

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

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


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

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

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

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

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


DEBUG:Going to execute:
auto

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

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

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

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


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