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 (r x y)
  ============================
   (R x y)


DEBUG:Going to execute:
destruct (X x y)

Goals:
  
  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 true
  r0 : R x y
  ============================
   (R x y)

  
  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:
auto
DEBUG LTAC Evaluated term: (X x y)

Goals:
  
  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 true
  r0 : R x y
  ============================
   (R x y)

  
  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::auto@0> $1 $2 $3