Goal:
    P : Type  Q : Type
  ============================
   (P <~> Q -> P -> Q)


DEBUG:Going to execute:
PTRDEBUGTAC<coq-core.plugins.ssreflect::ssrapply@0> $1