∀ {α : 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 α β) (x_1 : α)
  (h_1 :
    (fallback : α) →
      ((y : α_1) → rel Std.DTreeMap.Internal.Impl.leaf fallback y → β_1 y) →
        motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : α) →
              ((y : α_1) →
                  rel (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x y → β_1 y) →
                motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    (h : r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) →
                      (fallback : α) →
                        ((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))
                                fallback 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))
                            fallback),
  ((match (motive :=
        (x : Std.DTreeMap.Internal.Impl α β) → (x_2 : α) → ((y : α_1) → rel x x_2 y → β_1 y) → motive x x_2) x, x_1 with
      | Std.DTreeMap.Internal.Impl.leaf, fallback => fun x => h_1 fallback x
      | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => fun x_2 =>
        h_2 size k v l x x_2
      | 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),
        fallback => fun x => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback x)
      fun y h => f y) =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback fun y h => f y
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x 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),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback fun y h => f y