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


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

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