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


DEBUG:Going to execute:
intros [] []

Goals:
    P : Type  Q : Type  p : bool  q : P -> Q  p0 : Q -> P  p1 : P
  ============================
   (reflectT Q true)

    P : Type  Q : Type  p : bool  q : P -> Q  p0 : Q -> P  f : P -> False
  ============================
   (reflectT Q false)


DEBUG:Going to execute:
constructor

Goals:
    P : Type  Q : Type  p : bool  q : P -> Q  p0 : Q -> P  p1 : P
  ============================
   (reflectT Q true)

    P : Type  Q : Type  p : bool  q : P -> Q  p0 : Q -> P  f : P -> False
  ============================
   (reflectT Q false)


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>

Goals:
    P : Type  Q : Type  p : bool  q : P -> Q  p0 : Q -> P  p1 : P
  ============================
   Q

    P : Type  Q : Type  p : bool  q : P -> Q  p0 : Q -> P  f : P -> False
  ============================
   (Q -> False)


DEBUG:Going to execute:
auto

Goals:
    P : Type  Q : Type  p : bool  q : P -> Q  p0 : Q -> P  p1 : P
  ============================
   Q

    P : Type  Q : Type  p : bool  q : P -> Q  p0 : Q -> P  f : P -> False
  ============================
   (Q -> False)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3