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


DEBUG:Going to execute:
destruct 1

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

    A : Prop  n : ~ A
  ============================
   (reflectT A false)


DEBUG:Going to execute:
now constructor

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

    A : Prop  n : ~ A
  ============================
   (reflectT A false)


DEBUG:Going to execute:
constructor

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

    A : Prop  n : ~ A
  ============================
   (reflectT A false)


DEBUG:Going to execute:
t; easy

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

    A : Prop  n : ~ A
  ============================
   (reflectT A false)


DEBUG:Going to execute:
t

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

    A : Prop  n : ~ A
  ============================
   (reflectT A false)


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

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

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


DEBUG:Going to execute:
easy

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

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


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