Definition integerU64TWFDecidable (t : integerU64T) : {integerU64TWF t}+{~integerU64TWF t} :=
  inRangeDecidable (u64 t) u64Min u64Max.
