Goal:
  
  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'')


DEBUG:Going to execute:
inversion_clear H
DEBUG LTAC Evaluated term: hl'
DEBUG LTAC Evaluated term: hl'
DEBUG LTAC Evaluated term: hl'
DEBUG LTAC Evaluated term: hl'