Goal:
    P : Type  b : bool  H : P -> b  X : b -> P
  ============================
   (reflectT P b)


DEBUG:Going to execute:
destruct b; constructor