Goal:
  
  A : Type
  B : Type
  a : A
  l : list A
  P : B → Type
  x : B
  l0 : list B
  p : P x
  X : All P l0
  IHX : ∀ l : list A, #|l| = #|l0| → All2 (λ (_ : A) (b : B), P b) l l0
  H : S #|l| = S #|l0|
  ============================
   (All2 (λ (_ : A) (b : B), P b) (a :: l) (x :: l0))


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

Goals:
  
  A : Type
  B : Type
  a : A
  l : list A
  P : B → Type
  x : B
  l0 : list B
  p : P x
  X : All P l0
  IHX : ∀ l : list A, #|l| = #|l0| → All2 (λ (_ : A) (b : B), P b) l l0
  H : S #|l| = S #|l0|
  ============================
   (P x)

  
  A : Type
  B : Type
  a : A
  l : list A
  P : B → Type
  x : B
  l0 : list B
  p : P x
  X : All P l0
  IHX : ∀ l : list A, #|l| = #|l0| → All2 (λ (_ : A) (b : B), P b) l l0
  H : S #|l| = S #|l0|
  ============================
   (All2 (λ (_ : A) (b : B), P b) l l0)


DEBUG:Going to execute:
eauto

Goals:
  
  A : Type
  B : Type
  a : A
  l : list A
  P : B → Type
  x : B
  l0 : list B
  p : P x
  X : All P l0
  IHX : ∀ l : list A, #|l| = #|l0| → All2 (λ (_ : A) (b : B), P b) l l0
  H : S #|l| = S #|l0|
  ============================
   (P x)

  
  A : Type
  B : Type
  a : A
  l : list A
  P : B → Type
  x : B
  l0 : list B
  p : P x
  X : All P l0
  IHX : ∀ l : list A, #|l| = #|l0| → All2 (λ (_ : A) (b : B), P b) l l0
  H : S #|l| = S #|l0|
  ============================
   (All2 (λ (_ : A) (b : B), P b) l l0)


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