Goal:
    b : byte
  ============================
   (NoConfusion_byte b b)


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: (NoConfusion_byte b b)
DEBUG LTAC Evaluated term: Prop
Level 3: type of T
 has value 
Prop