Definition integerS16TWFDecidable (t : integerS16T) : {integerS16TWF t}+{~integerS16TWF t} :=
  inRangeDecidable (s16 t) s16Min s16Max.
