Definition integerU64TWF (t : integerU64T) : Prop :=
  isU64 (u64 t).
