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


DEBUG:Going to execute:
specialize (H1 eq_refl)
DEBUG LTAC Evaluated term: (H1 eq_refl)