Goal:
  
  A : Type
  B : Type
  A' : Type
  B' : Type
  R : A' → B' → Type
  f : nat → A → A'
  g : nat → B → B'
  x : A
  y : B
  l : list A
  l' : list B
  r : ∀ i : nat, R (f i x) (g i y)
  h : All2 (λ (x : A) (y : B), ∀ i : nat, R (f i x) (g i y)) l l'
  i : nat
  IHh : ∀ i : nat, All2 R (mapi_rec f l i) (mapi_rec g l' i)
  ============================
   (All2 R (f i x :: mapi_rec f l (S i)) (g i y :: mapi_rec g l' (S i)))


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

Goals:
  
  A : Type
  B : Type
  A' : Type
  B' : Type
  R : A' → B' → Type
  f : nat → A → A'
  g : nat → B → B'
  x : A
  y : B
  l : list A
  l' : list B
  r : ∀ i : nat, R (f i x) (g i y)
  h : All2 (λ (x : A) (y : B), ∀ i : nat, R (f i x) (g i y)) l l'
  i : nat
  IHh : ∀ i : nat, All2 R (mapi_rec f l i) (mapi_rec g l' i)
  ============================
   (R (f i x) (g i y))

  
  A : Type
  B : Type
  A' : Type
  B' : Type
  R : A' → B' → Type
  f : nat → A → A'
  g : nat → B → B'
  x : A
  y : B
  l : list A
  l' : list B
  r : ∀ i : nat, R (f i x) (g i y)
  h : All2 (λ (x : A) (y : B), ∀ i : nat, R (f i x) (g i y)) l l'
  i : nat
  IHh : ∀ i : nat, All2 R (mapi_rec f l i) (mapi_rec g l' i)
  ============================
   (All2 R (mapi_rec f l (S i)) (mapi_rec g l' (S i)))


DEBUG:Going to execute:
eauto

Goals:
  
  A : Type
  B : Type
  A' : Type
  B' : Type
  R : A' → B' → Type
  f : nat → A → A'
  g : nat → B → B'
  x : A
  y : B
  l : list A
  l' : list B
  r : ∀ i : nat, R (f i x) (g i y)
  h : All2 (λ (x : A) (y : B), ∀ i : nat, R (f i x) (g i y)) l l'
  i : nat
  IHh : ∀ i : nat, All2 R (mapi_rec f l i) (mapi_rec g l' i)
  ============================
   (R (f i x) (g i y))

  
  A : Type
  B : Type
  A' : Type
  B' : Type
  R : A' → B' → Type
  f : nat → A → A'
  g : nat → B → B'
  x : A
  y : B
  l : list A
  l' : list B
  r : ∀ i : nat, R (f i x) (g i y)
  h : All2 (λ (x : A) (y : B), ∀ i : nat, R (f i x) (g i y)) l l'
  i : nat
  IHh : ∀ i : nat, All2 R (mapi_rec f l i) (mapi_rec g l' i)
  ============================
   (All2 R (mapi_rec f l (S i)) (mapi_rec g l' (S i)))


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

Goals:
    A : Type  B : Type  R : A → B → Type  n : nat
  ============================
   (All2 R (skipn n []) (skipn n []))

  
  A : Type
  B : Type
  R : A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (All2 R (skipn n (x :: l)) (skipn n (y :: l')))


DEBUG:Going to execute:
destruct n; try econstructor
DEBUG LTAC Evaluated term: h

Goals:
    A : Type  B : Type  R : A → B → Type  n : nat
  ============================
   (All2 R (skipn n []) (skipn n []))

  
  A : Type
  B : Type
  R : A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (All2 R (skipn n (x :: l)) (skipn n (y :: l')))


DEBUG:Going to execute:
destruct n

Goals:
    A : Type  B : Type  R : A → B → Type
  ============================
   (All2 R (skipn 0 []) (skipn 0 []))

    A : Type  B : Type  R : A → B → Type  n : nat
  ============================
   (All2 R (skipn (S n) []) (skipn (S n) []))

  
  A : Type
  B : Type
  R : A → B → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (All2 R (skipn 0 (x :: l)) (skipn 0 (y :: l')))

  
  A : Type
  B : Type
  R : A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  h : All2 R l l'
  IHh : ∀ n : nat, All2 R (skipn n l) (skipn n l')
  ============================
   (All2 R (skipn (S n) (x :: l)) (skipn (S n) (y :: l')))


DEBUG:Going to execute:
try econstructor
DEBUG LTAC Evaluated term: n
DEBUG LTAC Evaluated term: n