Goal:
    A : Type  R : relation A  x : A  y : A  f : flip R x y
  ============================
   (clos_sym R y x)


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

Goals:
    A : Type  R : relation A  x : A  y : A  r : R x y
  ============================
   (flip R y x)

    A : Type  R : relation A  x : A  y : A  f : flip R x y
  ============================
   (R y x)


DEBUG:Going to execute:
assumption

Goals:
    A : Type  R : relation A  x : A  y : A  r : R x y
  ============================
   (flip R y x)

    A : Type  R : relation A  x : A  y : A  f : flip R x y
  ============================
   (R y x)


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