Goal:
    s : t  s' : t
  ============================
   (reflectProp (s = s') (eqb s s'))


DEBUG:Going to execute:
destruct (eqb s s') eqn:e

Goals:
    s : t  s' : t  e : eqb s s' = true
  ============================
   (reflectProp (s = s') true)

    s : t  s' : t  e : eqb s s' = false
  ============================
   (reflectProp (s = s') false)


DEBUG:Going to execute:
constructor
DEBUG LTAC Evaluated term: (eqb s s')

Goals:
    s : t  s' : t  e : eqb s s' = true
  ============================
   (reflectProp (s = s') true)

    s : t  s' : t  e : eqb s s' = false
  ============================
   (reflectProp (s = s') false)


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