Inductive integerS64T : Set := IntegerS64 {
  s64 : Z
}.
