Goal:
  
  A : Type
  R : crelation A
  HR : Transitive R
  x : A
  y : A
  z : A
  xy : R y x
  yz : R z y
  ============================
   (R z x)


DEBUG:Going to execute:
eapply HR
DEBUG LTAC Evaluated term: (fst ?p ?y ?y0 ?y1 ?y2 ?y3)
DEBUG LTAC Evaluated term: refl
DEBUG LTAC Evaluated term: sym
DEBUG LTAC Evaluated term: trans
DEBUG LTAC Evaluated term: refl
DEBUG LTAC Evaluated term: sym
DEBUG LTAC Evaluated term: trans
DEBUG LTAC Evaluated term: reflexivity
DEBUG LTAC Evaluated term: symmetry

Goals:
  
  A : Type
  R : crelation A
  HR : Transitive R
  x : A
  y : A
  z : A
  xy : R y x
  yz : R z y
  ============================
   (R z ?y)

  
  A : Type
  R : crelation A
  HR : Transitive R
  x : A
  y : A
  z : A
  xy : R y x
  yz : R z y
  ============================
   (R ?y x)


DEBUG:Going to execute:
eassumption
DEBUG LTAC Evaluated term: HR

Goals:
  
  A : Type
  R : crelation A
  HR : Transitive R
  x : A
  y : A
  z : A
  xy : R y x
  yz : R z y
  ============================
   (R z ?y)

  
  A : Type
  R : crelation A
  HR : Transitive R
  x : A
  y : A
  z : A
  xy : R y x
  yz : R z y
  ============================
   (R ?y x)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::eassumption@0>