Definition jsonKeyAssignment (k : keyAssignment) : json :=
  JsonObject [
    ("ID",                        JsonInteger (kaId k));
    ("KeyValueStart",             JsonInteger (kaValueStart k));
    ("KeyValueCenter",            JsonInteger (kaValueCenter k));
    ("KeyValueEnd",               JsonInteger (kaValueEnd k));
    ("ClipID",                    JsonInteger (kaClipId k));
    ("AmplitudeAtKeyStart",       float (kaAmplitudeAtKeyStart k));
    ("AmplitudeAtKeyCenter",      float (kaAmplitudeAtKeyCenter k));
    ("AmplitudeAtKeyEnd",         float (kaAmplitudeAtKeyEnd k));
    ("AtVelocityStart",           float (kaAtVelocityStart k));
    ("AtVelocityCenter",          float (kaAtVelocityCenter k));
    ("AtVelocityEnd",             float (kaAtVelocityEnd k));
    ("AmplitudeAtVelocityStart",  float (kaAmplitudeAtVelocityStart k));
    ("AmplitudeAtVelocityCenter", float (kaAmplitudeAtVelocityCenter k));
    ("AmplitudeAtVelocityEnd",    float (kaAmplitudeAtVelocityEnd k));
    ("Flags",                     JsonArray (map flagJson (kaFlags k)))
  ].
