Definition integerS16TWF (t : integerS16T) : Prop :=
  isS16 (s16 t).
