Definition integerU8TWFDecidable (t : integerU8T) : {integerU8TWF t}+{~integerU8TWF t} :=
  inRangeDecidable (u8 t) u8Min u8Max.
