{motive : Lean.Json.Structured → Sort u} →
  (t : Lean.Json.Structured) →
    ((elems : Array Lean.Json) → motive (Lean.Json.Structured.arr elems)) →
      ((kvPairs : Std.TreeMap.Raw String Lean.Json compare) → motive (Lean.Json.Structured.obj kvPairs)) → motive t