Goal:
    A : Prop  b : bool
  ============================
   (reflectT A b -> reflect A b)


DEBUG:Going to execute:
destruct 1

Goals:
    A : Prop  a : A
  ============================
   (reflect A true)

    A : Prop  f : A -> False
  ============================
   (reflect A false)


DEBUG:Going to execute:
now constructor

Goals:
    A : Prop  a : A
  ============================
   (reflect A true)

    A : Prop  f : A -> False
  ============================
   (reflect A false)


DEBUG:Going to execute:
constructor

Goals:
    A : Prop  a : A
  ============================
   (reflect A true)

    A : Prop  f : A -> False
  ============================
   (reflect A false)


DEBUG:Going to execute:
t; easy

Goals:
    A : Prop  a : A
  ============================
   (reflect A true)

    A : Prop  f : A -> False
  ============================
   (reflect A false)


DEBUG:Going to execute:
t

Goals:
    A : Prop  a : A
  ============================
   (reflect A true)

    A : Prop  f : A -> False
  ============================
   (reflect A false)


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

Goals:
    A : Prop  a : A
  ============================
   A

    A : Prop  f : A -> False
  ============================
   (~ A)


DEBUG:Going to execute:
easy

Goals:
    A : Prop  a : A
  ============================
   A

    A : Prop  f : A -> False
  ============================
   (~ A)


DEBUG:Going to execute:
easy0 || (solve [ intuition eauto  3 with core terms ])