Goal:
  
  A : Type
  f : A -> bool
  RA : ReflectEq A
  y : A
  hx : f y = true
  hy : f y = true
  H : hx = hy
  ============================
   (exist (fun z : A => f z = true) y hx =
    exist (fun z : A => f z = true) y hy)


DEBUG:Going to execute:
<coq-core.plugins.ltac::subst@1>
DEBUG LTAC Evaluated term: (uip hx hy)