Goal:
  
  a : byte
  b : byte
  H : eta_byte
        (fun b1 b2 : byte =>
         eta_byte (fun b3 : byte => if (b1 =? b3)%byte then True else False)
           b2) a b
  ============================
   (a = b)


DEBUG:Going to execute:
apply byte_dec_bl