Goal:
  
  ============================
   (false <-> true -> false = true)


DEBUG:Going to execute:
reflexivity
Level 1: Backtrace:

In environment
H : true <-> false
Unable to unify "false" with "true".
Level 0: Backtrace:

In environment
H : true <-> false
Unable to unify "false" with "true".