Definition integerU16TWFDecidable (t : integerU16T) : {integerU16TWF t}+{~integerU16TWF t} :=
  inRangeDecidable (u16 t) u16Min u16Max.
