Goal:
    H1 : false -> true  H2 : true -> false
  ============================
   (false = true)


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

Goals:
    H1 : is_true false  H2 : false -> true
  ============================
   (true = false)

    H1 : false -> true  H2 : true -> false
  ============================
   (false = true)


DEBUG:Going to execute:
try specialize (H2 eq_refl)
Level 0: Backtrace:

In environment
H1 : false -> true
H2 : true -> false
The term "eq_refl" has type "false = false" while it is expected to have type
 "is_true false" (cannot unify "false" and "true").
Level 0: Backtrace:

In environment
H1 : false -> true
H2 : true -> false
The term "eq_refl" has type "false = false" while it is expected to have type
 "is_true false" (cannot unify "false" and "true").