Goal:
    P : Type  Q : Type  p : bool
  ============================
   (CRelationClasses.iffT P Q -> reflectT P p -> reflectT Q p)


DEBUG:Going to execute:
intros [] []; constructor