Goal:
    b : bool  b' : bool
  ============================
   (b <-> b' -> b = b')


DEBUG:Going to execute:
destruct b, b'; cbnr; intros [H1 H2]; try specialize (H1 eq_refl)