Goal:
  
  A : Type
  B : Type
  P : B → A → A → Prop
  h : ∀ b : B, Transitive (P b)
  l0 : list B
  l : list A
  l' : list A
  l'' : list A
  hl : Forall3 P l0 l l'
  hl' : Forall3 P l0 l' l''
  ============================
   (Forall3 P l0 l l'')


DEBUG:Going to execute:
induction hl in l'', hl' |- *

Goals:
  
  A : Type
  B : Type
  P : B → A → A → Prop
  h : ∀ b : B, Transitive (P b)
  l'' : list A
  hl' : Forall3 P [] [] l''
  ============================
   (Forall3 P [] [] l'')

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


DEBUG:Going to execute:
inv hl'
DEBUG LTAC Evaluated term: hl

Goals:
  
  A : Type
  B : Type
  P : B → A → A → Prop
  h : ∀ b : B, Transitive (P b)
  l'' : list A
  hl' : Forall3 P [] [] l''
  ============================
   (Forall3 P [] [] l'')

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


DEBUG:Going to execute:
fun H => inversion_clear H