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
  hl' : Forall3 P [] [] []
  ============================
   (Forall3 P' [] [] [])


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'