Goal:
    a : byte  b : byte  H : if (a =? b)%byte then True else False
  ============================
   ((a =? b)%byte = true)


DEBUG:Going to execute:
destruct Byte.eqb
DEBUG LTAC Evaluated term: byte_dec_bl
DEBUG LTAC Evaluated term: uneta_byte
DEBUG LTAC Evaluated term: uneta_byte
DEBUG LTAC Evaluated term: uneta_byte
DEBUG LTAC Evaluated term: uneta_byte