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


DEBUG:Going to execute:
rewrite <- Byte.of_to_N
DEBUG LTAC Evaluated term: (Some x = Some y)