Goal:
  
  A : Type
  B : Type
  P : B → A → A → Prop
  P' : B → A → A → Prop
  h : ∀ (b : B) (x y : A), P b x y → P b y x → P' b x y
  x : B
  y : A
  z : A
  l : list B
  l' : list A
  l'' : list A
  H : P x y z
  hl : Forall3 P l l' l''
  hl' : Forall3 P (x :: l) (z :: l'') (y :: l')
  IHhl : Forall3 P l l'' l' → Forall3 P' l l' l''
  ============================
   (Forall3 P' (x :: l) (y :: l') (z :: l''))


DEBUG:Going to execute:
inversion_clear H
Level 1: evaluation returns
inversion_clear H
where
H := hl'
of type
constr of type tacvalue


Goals:
  
  A : Type
  B : Type
  P : B → A → A → Prop
  P' : B → A → A → Prop
  h : ∀ (b : B) (x y : A), P b x y → P b y x → P' b x y
  ============================
   (Forall3 P' [] [] [])

  
  A : Type
  B : Type
  P : B → A → A → Prop
  P' : B → A → A → Prop
  h : ∀ (b : B) (x y : A), P b x y → P b y x → P' b x y
  x : B
  y : A
  z : A
  l : list B
  l' : list A
  l'' : list A
  H : P x y z
  hl : Forall3 P l l' l''
  IHhl : Forall3 P l l'' l' → Forall3 P' l l' l''
  H0 : P x z y
  H1 : Forall3 P l l'' l'
  ============================
   (Forall3 P' (x :: l) (y :: l') (z :: l''))


DEBUG:Going to execute:
constructor
Level 1: evaluation returns
inversion_clear H
where
H := hl'
of type
constr of type tacvalue


Goals:
  
  A : Type
  B : Type
  P : B → A → A → Prop
  P' : B → A → A → Prop
  h : ∀ (b : B) (x y : A), P b x y → P b y x → P' b x y
  ============================
   (Forall3 P' [] [] [])

  
  A : Type
  B : Type
  P : B → A → A → Prop
  P' : B → A → A → Prop
  h : ∀ (b : B) (x y : A), P b x y → P b y x → P' b x y
  x : B
  y : A
  z : A
  l : list B
  l' : list A
  l'' : list A
  H : P x y z
  hl : Forall3 P l l' l''
  IHhl : Forall3 P l l'' l' → Forall3 P' l l' l''
  H0 : P x z y
  H1 : Forall3 P l l'' l'
  ============================
   (Forall3 P' (x :: l) (y :: l') (z :: l''))


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

Goals:
  
  A : Type
  B : Type
  P : B → A → A → Prop
  P' : B → A → A → Prop
  h : ∀ (b : B) (x y : A), P b x y → P b y x → P' b x y
  x : B
  y : A
  z : A
  l : list B
  l' : list A
  l'' : list A
  H : P x y z
  hl : Forall3 P l l' l''
  IHhl : Forall3 P l l'' l' → Forall3 P' l l' l''
  H0 : P x z y
  H1 : Forall3 P l l'' l'
  ============================
   (P' x y z)

  
  A : Type
  B : Type
  P : B → A → A → Prop
  P' : B → A → A → Prop
  h : ∀ (b : B) (x y : A), P b x y → P b y x → P' b x y
  x : B
  y : A
  z : A
  l : list B
  l' : list A
  l'' : list A
  H : P x y z
  hl : Forall3 P l l' l''
  IHhl : Forall3 P l l'' l' → Forall3 P' l l' l''
  H0 : P x z y
  H1 : Forall3 P l l'' l'
  ============================
   (Forall3 P' l l' l'')


DEBUG:Going to execute:
eauto

Goals:
  
  A : Type
  B : Type
  P : B → A → A → Prop
  P' : B → A → A → Prop
  h : ∀ (b : B) (x y : A), P b x y → P b y x → P' b x y
  x : B
  y : A
  z : A
  l : list B
  l' : list A
  l'' : list A
  H : P x y z
  hl : Forall3 P l l' l''
  IHhl : Forall3 P l l'' l' → Forall3 P' l l' l''
  H0 : P x z y
  H1 : Forall3 P l l'' l'
  ============================
   (P' x y z)

  
  A : Type
  B : Type
  P : B → A → A → Prop
  P' : B → A → A → Prop
  h : ∀ (b : B) (x y : A), P b x y → P b y x → P' b x y
  x : B
  y : A
  z : A
  l : list B
  l' : list A
  l'' : list A
  H : P x y z
  hl : Forall3 P l l' l''
  IHhl : Forall3 P l l'' l' → Forall3 P' l l' l''
  H0 : P x z y
  H1 : Forall3 P l l'' l'
  ============================
   (Forall3 P' l l' l'')


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