{motive_1 : Lean.Json → Sort u} →
  {motive_2 : Array Lean.Json → Sort u} →
    {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} →
      {motive_4 : List Lean.Json → Sort u} →
        {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u} →
          {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u} →
            motive_1 Lean.Json.null →
              ((b : Bool) → motive_1 (Lean.Json.bool b)) →
                ((n : Lean.JsonNumber) → motive_1 (Lean.Json.num n)) →
                  ((s : String) → motive_1 (Lean.Json.str s)) →
                    ((elems : Array Lean.Json) → motive_2 elems → motive_1 (Lean.Json.arr elems)) →
                      ((kvPairs : Std.TreeMap.Raw String Lean.Json compare) →
                          motive_3 kvPairs → motive_1 (Lean.Json.obj kvPairs)) →
                        ((toList : List Lean.Json) → motive_4 toList → motive_2 { toList := toList }) →
                          ((inner : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) →
                              motive_5 inner → motive_3 { inner := inner }) →
                            motive_4 [] →
                              ((head : Lean.Json) →
                                  (tail : List Lean.Json) → motive_1 head → motive_4 tail → motive_4 (head :: tail)) →
                                ((inner : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) →
                                    motive_6 inner → motive_5 { inner := inner }) →
                                  ((size : ℕ) →
                                      (k : String) →
                                        (v : (fun x => Lean.Json) k) →
                                          (l r : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) →
                                            motive_1 v →
                                              motive_6 l →
                                                motive_6 r → motive_6 (Std.DTreeMap.Internal.Impl.inner size k v l r)) →
                                    motive_6 Std.DTreeMap.Internal.Impl.leaf → (t : List Lean.Json) → motive_4 t