Definition integerU32TWF (t : integerU32T) : Prop :=
  isU32 (u32 t).
