(motive : Lean.Json → Sort u_1) →
  (x : Lean.Json) →
    (Unit → motive Lean.Json.null) →
      ((b : Bool) → motive (Lean.Json.bool b)) →
        ((n : Lean.JsonNumber) → motive (Lean.Json.num n)) →
          ((s : String) → motive (Lean.Json.str s)) →
            ((elems : Array Lean.Json) → motive (Lean.Json.arr elems)) →
              ((kvPairs : Std.TreeMap.Raw String Lean.Json compare) → motive (Lean.Json.obj kvPairs)) → motive x