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