{α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β) →
                  (r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r)) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (size_1 : ℕ) →
                      (k_1 : α) →
                        (v_1 : β) →
                          (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner size k v
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)) →
              motive x