Definition integerS8TWFDecidable (t : integerS8T) : {integerS8TWF t}+{~integerS8TWF t} :=
  inRangeDecidable (s8 t) s8Min s8Max.
