Definition integerS64TWFDecidable (t : integerS64T) : {integerS64TWF t}+{~integerS64TWF t} :=
  inRangeDecidable (s64 t) s64Min s64Max.
