Goal:
    x : byte  y : byte
  ============================
   (reflectProp (x = y) match compare x y with
                        | Eq => true
                        | _ => false
                        end)


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

Goals:
    x : byte  y : byte  H : x = y
  ============================
   (reflectProp (x = y) true)

    x : byte  y : byte  H : lt x y
  ============================
   (reflectProp (x = y) false)

    x : byte  y : byte  H : lt y x
  ============================
   (reflectProp (x = y) false)


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

Goals:
    x : byte  y : byte  H : x = y
  ============================
   (reflectProp (x = y) true)

    x : byte  y : byte  H : lt x y
  ============================
   (reflectProp (x = y) false)

    x : byte  y : byte  H : lt y x
  ============================
   (reflectProp (x = y) false)


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

Goals:
    x : byte  y : byte  H : x = y
  ============================
   (x = y)

    x : byte  y : byte  H : lt x y
  ============================
   (x <> y)

    x : byte  y : byte  H : lt y x
  ============================
   (x <> y)


DEBUG:Going to execute:
auto

Goals:
    x : byte  y : byte  H : x = y
  ============================
   (x = y)

    x : byte  y : byte  H : lt x y
  ============================
   (x <> y)

    x : byte  y : byte  H : lt y x
  ============================
   (x <> y)


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