Inductive integerU64T : Set := IntegerU64 {
  u64 : Z
}.
