Goal:
    x : t  y : t
  ============================
   (reflectProp (x = y) (eqb x y))


DEBUG:Going to execute:
match goal with
           | H:exists y, _ y |- _ => tac H
           | H:{x : _ | ?P x} |- _ => tac H
           | H:{x : _ & ?P x} |- _ => tacT H
           | H:exists2 x : _, _ x & _ x |- _ => tac2 H
           | H:{x : _ | ?P x & _ x} |- _ => tac2 H
           | H:{x : _ & ?P x & _ x} |- _ => tacT2 H
           end