Definition jsonLoopRange (lr : loopRange) : json :=
  JsonObject [
    ("FrameStart",        JsonInteger (lrFrameStart lr));
    ("FrameEndInclusive", JsonInteger (lrFrameEndInclusive lr)) 
  ].
