Goal:
  
  A : Type
  R : A -> A -> Type
  r : A -> A -> bool
  X : forall x y : A, reflectT (R x y) (r x y)
  x : A
  y : A
  h : is_true false
  f : R x y -> False
  ============================
   (R x y)


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