Goal:
    G : t  HI : invariants  A : Prop  B : Prop  H : A <-> B  f : bool
  ============================
   (ssrbool.reflect B f -> ssrbool.reflect A f)


DEBUG:Going to execute:
destruct 1; constructor