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


DEBUG:Going to execute:
unfold eq_sig_true