∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (α_1 : Sort u✝)
  (β_1 : α_1 → Sort v✝) (f : (x : α_1) → β_1 x) (rel : (Std.DTreeMap.Internal.Impl α fun x => β) → α_1 → Prop)
  (x : Std.DTreeMap.Internal.Impl α fun x => β)
  (h_1 : Unit → ((y : α_1) → rel Std.DTreeMap.Internal.Impl.leaf y → β_1 y) → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            ((y : α_1) → rel (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) y → β_1 y) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    (h : r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) →
                      ((y : α_1) →
                          rel
                              (Std.DTreeMap.Internal.Impl.inner size k v l
                                (namedPattern r (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) h))
                              y →
                            β_1 y) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (namedPattern r (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) h))),
  ((match (motive := (x : Std.DTreeMap.Internal.Impl α fun x => β) → ((y : α_1) → rel x y → β_1 y) → motive x) x with
      | Std.DTreeMap.Internal.Impl.leaf => fun x => h_1 a x
      | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => fun x => h_2 size k v l x
      | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
        fun x => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h x)
      fun y h => f y) =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 a fun y h => f y
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l fun y h => f y
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fun y h => f y