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


DEBUG:Going to execute:
induction hl; constructor