Inductive integerS8T : Set := IntegerS8 {
  s8 : Z
}.
