Goal:
    b : bool  b' : bool
  ============================
   (b <-> b' -> b = b')


DEBUG:Going to execute:
destruct b, b'

Goals:
  
  ============================
   (true <-> true -> true = true)

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

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

  
  ============================
   (false <-> false -> false = false)


DEBUG:Going to execute:
cbnr
DEBUG LTAC Evaluated term: b
DEBUG LTAC Evaluated term: b'
DEBUG LTAC Evaluated term: b'

Goals:
  
  ============================
   (true <-> true -> true = true)

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

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

  
  ============================
   (false <-> false -> false = false)


DEBUG:Going to execute:
cbn; try reflexivity

Goals:
  
  ============================
   (true <-> true -> true = true)

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

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

  
  ============================
   (false <-> false -> false = false)


DEBUG:Going to execute:
cbn

Goals:
  
  ============================
   (true <-> true -> true = true)

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

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

  
  ============================
   (false <-> false -> false = false)


DEBUG:Going to execute:
try reflexivity