Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Δ : list A) (x : A), P Δ Δ x x
  ============================
   (∀ Δ : list A, All2_fold P Δ Δ)


DEBUG:Going to execute:
induction Δ

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Δ : list A) (x : A), P Δ Δ x x
  ============================
   (All2_fold P [] [])

  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Δ : list A) (x : A), P Δ Δ x x
  a : A
  Δ : list A
  IHΔ : All2_fold P Δ Δ
  ============================
   (All2_fold P (a :: Δ) (a :: Δ))


DEBUG:Going to execute:
constructor

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Δ : list A) (x : A), P Δ Δ x x
  ============================
   (All2_fold P [] [])

  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Δ : list A) (x : A), P Δ Δ x x
  a : A
  Δ : list A
  IHΔ : All2_fold P Δ Δ
  ============================
   (All2_fold P (a :: Δ) (a :: Δ))


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

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Δ : list A) (x : A), P Δ Δ x x
  a : A
  Δ : list A
  IHΔ : All2_fold P Δ Δ
  ============================
   (All2_fold P Δ Δ)

  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Δ : list A) (x : A), P Δ Δ x x
  a : A
  Δ : list A
  IHΔ : All2_fold P Δ Δ
  ============================
   (P Δ Δ a a)


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Δ : list A) (x : A), P Δ Δ x x
  a : A
  Δ : list A
  IHΔ : All2_fold P Δ Δ
  ============================
   (All2_fold P Δ Δ)

  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Δ : list A) (x : A), P Δ Δ x x
  a : A
  Δ : list A
  IHΔ : All2_fold P Δ Δ
  ============================
   (P Δ Δ a a)


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