Definition integerS8TWF (t : integerS8T) : Prop :=
  isS8 (s8 t).
