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


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

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

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