Goal:
  
  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
  IHhl : ∀ l'' : list A, Forall3 P l l''0 l'' → Forall3 P l l' l''
  z0 : A
  l''1 : list A
  H0 : P x z z0
  H1 : Forall3 P l l''0 l''1
  ============================
   (P x y ?y)


DEBUG:Going to execute:
assert X2
Level 1: evaluation returns
assert X2; [ exact (id0 id1) | clear id0 ]
where
id1 := x
of type
intropattern
id0 := P
of type
intropattern
flags := 
of type
tauto_flags
X2 := A → A → Prop
of type
constr of type tacvalue