Definition integerS64TWF (t : integerS64T) : Prop :=
  isS64 (s64 t).
