Definition integerU8TWF (t : integerU8T) : Prop :=
  isU8 (u8 t).
