Goal:
    A : Type  E : EqDec A  x : A  y : A
  ============================
   (reflectProp (x = y) (eq_dec_to_bool x y))


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3

Goals:
    A : Type  E : EqDec A  x : A  y : A  e : x = y
  ============================
   (reflectProp (x = y) true)

    A : Type  E : EqDec A  x : A  y : A  n : x <> y
  ============================
   (reflectProp (x = y) false)


DEBUG:Going to execute:
constructor
DEBUG LTAC Evaluated term: (eq_dec x y)

Goals:
    A : Type  E : EqDec A  x : A  y : A  e : x = y
  ============================
   (reflectProp (x = y) true)

    A : Type  E : EqDec A  x : A  y : A  n : x <> y
  ============================
   (reflectProp (x = y) false)


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

Goals:
    A : Type  E : EqDec A  x : A  y : A  e : x = y
  ============================
   (x = y)

    A : Type  E : EqDec A  x : A  y : A  n : x <> y
  ============================
   (x <> y)


DEBUG:Going to execute:
assumption

Goals:
    A : Type  E : EqDec A  x : A  y : A  e : x = y
  ============================
   (x = y)

    A : Type  E : EqDec A  x : A  y : A  n : x <> y
  ============================
   (x <> y)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::assumption@0>