Goal:
  
  A : Type
  P : A → A → Prop
  hP : Transitive P
  l3 : list A
  x : A
  y : A
  l : list A
  l' : list A
  H : P x y
  h1 : Forall2 P l l'
  h2 : Forall2 P (y :: l') l3
  IHh1 : ∀ l3 : list A, Forall2 P l' l3 → Forall2 P l l3
  x0 : A
  y0 : A
  l0 : list A
  l'0 : list A
  H2 : P y y0
  H4 : Forall2 P l' l'0
  H0 : x0 = y
  H1 : l0 = l'
  H3 : y0 :: l'0 = l3
  ============================
   (P x y0)


DEBUG:Going to execute:
eapply hP

Goals:
  
  A : Type
  P : A → A → Prop
  hP : Transitive P
  l3 : list A
  x : A
  y : A
  l : list A
  l' : list A
  H : P x y
  h1 : Forall2 P l l'
  h2 : Forall2 P (y :: l') l3
  IHh1 : ∀ l3 : list A, Forall2 P l' l3 → Forall2 P l l3
  x0 : A
  y0 : A
  l0 : list A
  l'0 : list A
  H2 : P y y0
  H4 : Forall2 P l' l'0
  H0 : x0 = y
  H1 : l0 = l'
  H3 : y0 :: l'0 = l3
  ============================
   (P x ?y)

  
  A : Type
  P : A → A → Prop
  hP : Transitive P
  l3 : list A
  x : A
  y : A
  l : list A
  l' : list A
  H : P x y
  h1 : Forall2 P l l'
  h2 : Forall2 P (y :: l') l3
  IHh1 : ∀ l3 : list A, Forall2 P l' l3 → Forall2 P l l3
  x0 : A
  y0 : A
  l0 : list A
  l'0 : list A
  H2 : P y y0
  H4 : Forall2 P l' l'0
  H0 : x0 = y
  H1 : l0 = l'
  H3 : y0 :: l'0 = l3
  ============================
   (P ?y y0)


DEBUG:Going to execute:
eauto
DEBUG LTAC Evaluated term: hP

Goals:
  
  A : Type
  P : A → A → Prop
  hP : Transitive P
  l3 : list A
  x : A
  y : A
  l : list A
  l' : list A
  H : P x y
  h1 : Forall2 P l l'
  h2 : Forall2 P (y :: l') l3
  IHh1 : ∀ l3 : list A, Forall2 P l' l3 → Forall2 P l l3
  x0 : A
  y0 : A
  l0 : list A
  l'0 : list A
  H2 : P y y0
  H4 : Forall2 P l' l'0
  H0 : x0 = y
  H1 : l0 = l'
  H3 : y0 :: l'0 = l3
  ============================
   (P x ?y)

  
  A : Type
  P : A → A → Prop
  hP : Transitive P
  l3 : list A
  x : A
  y : A
  l : list A
  l' : list A
  H : P x y
  h1 : Forall2 P l l'
  h2 : Forall2 P (y :: l') l3
  IHh1 : ∀ l3 : list A, Forall2 P l' l3 → Forall2 P l l3
  x0 : A
  y0 : A
  l0 : list A
  l'0 : list A
  H2 : P y y0
  H4 : Forall2 P l' l'0
  H0 : x0 = y
  H1 : l0 = l'
  H3 : y0 :: l'0 = l3
  ============================
   (P ?y y0)


DEBUG:Going to execute:
<coq-core.plugins.ltac::eauto@0> $1 $2 $3