Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  Γ : list A
  Δ : list A
  ============================
   (All2_fold (λ _ _ : list A, Q) Γ Δ <~> All2 Q Γ Δ)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::split@0>

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  Γ : list A
  Δ : list A
  ============================
   (All2_fold (λ _ _ : list A, Q) Γ Δ → All2 Q Γ Δ)

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  Γ : list A
  Δ : list A
  ============================
   (All2 Q Γ Δ → All2_fold (λ _ _ : list A, Q) Γ Δ)


DEBUG:Going to execute:
induction 1

Goals:
    A : Type  P : list A → list A → A → A → Type  Q : A → A → Type
  ============================
   (All2 Q [] [])

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  X : All2_fold (λ _ _ : list A, Q) Γ Γ'
  p : Q d d'
  IHX : All2 Q Γ Γ'
  ============================
   (All2 Q (d :: Γ) (d' :: Γ'))

    A : Type  P : list A → list A → A → A → Type  Q : A → A → Type
  ============================
   (All2_fold (λ _ _ : list A, Q) [] [])

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  x : A
  y : A
  l : list A
  l' : list A
  r : Q x y
  X : All2 Q l l'
  IHX : All2_fold (λ _ _ : list A, Q) l l'
  ============================
   (All2_fold (λ _ _ : list A, Q) (x :: l) (y :: l'))


DEBUG:Going to execute:
simpl

Goals:
    A : Type  P : list A → list A → A → A → Type  Q : A → A → Type
  ============================
   (All2 Q [] [])

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  X : All2_fold (λ _ _ : list A, Q) Γ Γ'
  p : Q d d'
  IHX : All2 Q Γ Γ'
  ============================
   (All2 Q (d :: Γ) (d' :: Γ'))

    A : Type  P : list A → list A → A → A → Type  Q : A → A → Type
  ============================
   (All2_fold (λ _ _ : list A, Q) [] [])

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  x : A
  y : A
  l : list A
  l' : list A
  r : Q x y
  X : All2 Q l l'
  IHX : All2_fold (λ _ _ : list A, Q) l l'
  ============================
   (All2_fold (λ _ _ : list A, Q) (x :: l) (y :: l'))


DEBUG:Going to execute:
constructor

Goals:
    A : Type  P : list A → list A → A → A → Type  Q : A → A → Type
  ============================
   (All2 Q [] [])

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  X : All2_fold (λ _ _ : list A, Q) Γ Γ'
  p : Q d d'
  IHX : All2 Q Γ Γ'
  ============================
   (All2 Q (d :: Γ) (d' :: Γ'))

    A : Type  P : list A → list A → A → A → Type  Q : A → A → Type
  ============================
   (All2_fold (λ _ _ : list A, Q) [] [])

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  x : A
  y : A
  l : list A
  l' : list A
  r : Q x y
  X : All2 Q l l'
  IHX : All2_fold (λ _ _ : list A, Q) l l'
  ============================
   (All2_fold (λ _ _ : list A, Q) (x :: l) (y :: l'))


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

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  X : All2_fold (λ _ _ : list A, Q) Γ Γ'
  p : Q d d'
  IHX : All2 Q Γ Γ'
  ============================
   (Q d d')

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  X : All2_fold (λ _ _ : list A, Q) Γ Γ'
  p : Q d d'
  IHX : All2 Q Γ Γ'
  ============================
   (All2 Q Γ Γ')

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  x : A
  y : A
  l : list A
  l' : list A
  r : Q x y
  X : All2 Q l l'
  IHX : All2_fold (λ _ _ : list A, Q) l l'
  ============================
   (All2_fold (λ _ _ : list A, Q) l l')

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  x : A
  y : A
  l : list A
  l' : list A
  r : Q x y
  X : All2 Q l l'
  IHX : All2_fold (λ _ _ : list A, Q) l l'
  ============================
   (Q x y)


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  X : All2_fold (λ _ _ : list A, Q) Γ Γ'
  p : Q d d'
  IHX : All2 Q Γ Γ'
  ============================
   (Q d d')

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  X : All2_fold (λ _ _ : list A, Q) Γ Γ'
  p : Q d d'
  IHX : All2 Q Γ Γ'
  ============================
   (All2 Q Γ Γ')

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  x : A
  y : A
  l : list A
  l' : list A
  r : Q x y
  X : All2 Q l l'
  IHX : All2_fold (λ _ _ : list A, Q) l l'
  ============================
   (All2_fold (λ _ _ : list A, Q) l l')

  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  x : A
  y : A
  l : list A
  l' : list A
  r : Q x y
  X : All2 Q l l'
  IHX : All2_fold (λ _ _ : list A, Q) l l'
  ============================
   (Q x y)


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