Definition integerU16TWF (t : integerU16T) : Prop :=
  isU16 (u16 t).
