Definition integerU32TWFDecidable (t : integerU32T) : {integerU32TWF t}+{~integerU32TWF t} :=
  inRangeDecidable (u32 t) u32Min u32Max.
