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


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>