Goal:
  
  A : Type
  B : Type
  C : Type
  D : Type
  R : nat → A → B → Type
  l : list C
  l' : list D
  f : nat → C → A
  g : nat → D → B
  n : nat
  ============================
   (All2i (λ (n : nat) (x : C) (y : D), R n (f n x) (g n y)) n l l'
    → All2i R n (mapi_rec f l n) (mapi_rec g l' n))


DEBUG:Going to execute:
induction 1

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

  
  A : Type
  B : Type
  C : Type
  D : Type
  R : nat → A → B → Type
  f : nat → C → A
  g : nat → D → B
  n : nat
  x : C
  y : D
  l : list C
  r : list D
  r0 : R n (f n x) (g n y)
  X : All2i (λ (n : nat) (x : C) (y : D), R n (f n x) (g n y)) (S n) l r
  IHX : All2i R (S n) (mapi_rec f l (S n)) (mapi_rec g r (S n))
  ============================
   (All2i R n (mapi_rec f (x :: l) n) (mapi_rec g (y :: r) n))


DEBUG:Going to execute:
constructor

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

  
  A : Type
  B : Type
  C : Type
  D : Type
  R : nat → A → B → Type
  f : nat → C → A
  g : nat → D → B
  n : nat
  x : C
  y : D
  l : list C
  r : list D
  r0 : R n (f n x) (g n y)
  X : All2i (λ (n : nat) (x : C) (y : D), R n (f n x) (g n y)) (S n) l r
  IHX : All2i R (S n) (mapi_rec f l (S n)) (mapi_rec g r (S n))
  ============================
   (All2i R n (mapi_rec f (x :: l) n) (mapi_rec g (y :: r) n))


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>

Goals:
  
  A : Type
  B : Type
  C : Type
  D : Type
  R : nat → A → B → Type
  f : nat → C → A
  g : nat → D → B
  n : nat
  x : C
  y : D
  l : list C
  r : list D
  r0 : R n (f n x) (g n y)
  X : All2i (λ (n : nat) (x : C) (y : D), R n (f n x) (g n y)) (S n) l r
  IHX : All2i R (S n) (mapi_rec f l (S n)) (mapi_rec g r (S n))
  ============================
   (R n (f n x) (g n y))

  
  A : Type
  B : Type
  C : Type
  D : Type
  R : nat → A → B → Type
  f : nat → C → A
  g : nat → D → B
  n : nat
  x : C
  y : D
  l : list C
  r : list D
  r0 : R n (f n x) (g n y)
  X : All2i (λ (n : nat) (x : C) (y : D), R n (f n x) (g n y)) (S n) l r
  IHX : All2i R (S n) (mapi_rec f l (S n)) (mapi_rec g r (S n))
  ============================
   (All2i R (S n)
      ((fix mapi_rec
          (A B : Type) (f : nat → A → B) (l : list A) (n : nat) {struct l} :
            list B :=
          match l with
          | [] => []
          | hd :: tl => f n hd :: mapi_rec A B f tl (S n)
          end) C A f l (S n))
      ((fix mapi_rec
          (A B : Type) (f : nat → A → B) (l : list A) (n : nat) {struct l} :
            list B :=
          match l with
          | [] => []
          | hd :: tl => f n hd :: mapi_rec A B f tl (S n)
          end) D B g r (S n)))


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  B : Type
  C : Type
  D : Type
  R : nat → A → B → Type
  f : nat → C → A
  g : nat → D → B
  n : nat
  x : C
  y : D
  l : list C
  r : list D
  r0 : R n (f n x) (g n y)
  X : All2i (λ (n : nat) (x : C) (y : D), R n (f n x) (g n y)) (S n) l r
  IHX : All2i R (S n) (mapi_rec f l (S n)) (mapi_rec g r (S n))
  ============================
   (R n (f n x) (g n y))

  
  A : Type
  B : Type
  C : Type
  D : Type
  R : nat → A → B → Type
  f : nat → C → A
  g : nat → D → B
  n : nat
  x : C
  y : D
  l : list C
  r : list D
  r0 : R n (f n x) (g n y)
  X : All2i (λ (n : nat) (x : C) (y : D), R n (f n x) (g n y)) (S n) l r
  IHX : All2i R (S n) (mapi_rec f l (S n)) (mapi_rec g r (S n))
  ============================
   (All2i R (S n)
      ((fix mapi_rec
          (A B : Type) (f : nat → A → B) (l : list A) (n : nat) {struct l} :
            list B :=
          match l with
          | [] => []
          | hd :: tl => f n hd :: mapi_rec A B f tl (S n)
          end) C A f l (S n))
      ((fix mapi_rec
          (A B : Type) (f : nat → A → B) (l : list A) (n : nat) {struct l} :
            list B :=
          match l with
          | [] => []
          | hd :: tl => f n hd :: mapi_rec A B f tl (S n)
          end) D B g r (S n)))


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