Definition integerS32TWF (t : integerS32T) : Prop :=
  isS32 (s32 t).
