Definition jsonIndexType (i : indexTypeT) : json :=
  JsonString match i with
  | INDEX_8  => "INDEX_8"
  | INDEX_16 => "INDEX_16"
  | INDEX_32 => "INDEX_32"
  end.
