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 : is_true false
  ============================
   (false = true)


DEBUG:Going to execute:
discriminate
DEBUG LTAC Evaluated term: (H2 eq_refl)

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

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


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

COQC theories/MCFSets.v