Goal:
    x : Byte.byte  y : Byte.byte  H : Byte.to_N x = Byte.to_N y
  ============================
   (Byte.of_N (Byte.to_N x) = Some y)


DEBUG:Going to execute:
rewrite <- Byte.of_to_N
DEBUG LTAC Evaluated term: Byte.of_to_N
DEBUG LTAC Evaluated term: Byte.of_to_N