Goal:
  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  l : list A
  l' : list B
  l'' : list B
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  ============================
   (OnOne2All P l l' l'' → All3 Q l l' l'')


DEBUG:Going to execute:
induction 1

Goals:
  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  hd' : B
  tl : list B
  p : P b hd hd'
  e : #|bs| = #|tl|
  ============================
   (All3 Q (b :: bs) (hd :: tl) (hd' :: tl))

  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  tl : list B
  tl' : list B
  X : OnOne2All P bs tl tl'
  IHX : All3 Q bs tl tl'
  ============================
   (All3 Q (b :: bs) (hd :: tl) (hd :: tl'))


DEBUG:Going to execute:
simpl

Goals:
  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  hd' : B
  tl : list B
  p : P b hd hd'
  e : #|bs| = #|tl|
  ============================
   (All3 Q (b :: bs) (hd :: tl) (hd' :: tl))

  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  tl : list B
  tl' : list B
  X : OnOne2All P bs tl tl'
  IHX : All3 Q bs tl tl'
  ============================
   (All3 Q (b :: bs) (hd :: tl) (hd :: tl'))


DEBUG:Going to execute:
constructor

Goals:
  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  hd' : B
  tl : list B
  p : P b hd hd'
  e : #|bs| = #|tl|
  ============================
   (All3 Q (b :: bs) (hd :: tl) (hd' :: tl))

  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  tl : list B
  tl' : list B
  X : OnOne2All P bs tl tl'
  IHX : All3 Q bs tl tl'
  ============================
   (All3 Q (b :: bs) (hd :: tl) (hd :: tl'))


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

Goals:
  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  hd' : B
  tl : list B
  p : P b hd hd'
  e : #|bs| = #|tl|
  ============================
   (Q b hd hd')

  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  hd' : B
  tl : list B
  p : P b hd hd'
  e : #|bs| = #|tl|
  ============================
   (All3 Q bs tl tl)

  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  tl : list B
  tl' : list B
  X : OnOne2All P bs tl tl'
  IHX : All3 Q bs tl tl'
  ============================
   (Q b hd hd)

  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  tl : list B
  tl' : list B
  X : OnOne2All P bs tl tl'
  IHX : All3 Q bs tl tl'
  ============================
   (All3 Q bs tl tl')


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  hd' : B
  tl : list B
  p : P b hd hd'
  e : #|bs| = #|tl|
  ============================
   (Q b hd hd')

  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  hd' : B
  tl : list B
  p : P b hd hd'
  e : #|bs| = #|tl|
  ============================
   (All3 Q bs tl tl)

  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  tl : list B
  tl' : list B
  X : OnOne2All P bs tl tl'
  IHX : All3 Q bs tl tl'
  ============================
   (Q b hd hd)

  
  A : Type
  B : Type
  P : A → B → B → Type
  Q : A → B → B → Type
  H1 : ∀ (x : A) (y z : B), P x y z → Q x y z
  H2 : ∀ (x : A) (y : B), Q x y y
  b : A
  bs : list A
  hd : B
  tl : list B
  tl' : list B
  X : OnOne2All P bs tl tl'
  IHX : All3 Q bs tl tl'
  ============================
   (All3 Q bs tl tl')


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