Definition integerS32TWFDecidable (t : integerS32T) : {integerS32TWF t}+{~integerS32TWF t} :=
  inRangeDecidable (s32 t) s32Min s32Max.
