∀ {α : Type u_1} {β : α → Type u_2} {δ : Type u_4} [inst : Ord α] (k : α)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      ((c : Std.DTreeMap.Internal.Cell α β (compare k)) →
          (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → δ) →
        Sort u_3)
  (size : ℕ) (k' : α) (v' : β k') (l r : Std.DTreeMap.Internal.Impl α β)
  (f :
    (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
      (Std.DTreeMap.Internal.Impl.contains' (compare k) (Std.DTreeMap.Internal.Impl.inner size k' v' l r) = true →
          c.contains = true) →
        δ)
  (h_1 :
    (f :
        (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
          (Std.DTreeMap.Internal.Impl.contains' (compare k) Std.DTreeMap.Internal.Impl.leaf = true →
              c.contains = true) →
            δ) →
      motive Std.DTreeMap.Internal.Impl.leaf f)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (f :
                (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
                  (Std.DTreeMap.Internal.Impl.contains' (compare k) (Std.DTreeMap.Internal.Impl.inner size k' v' l r) =
                        true →
                      c.contains = true) →
                    δ) →
              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r) f),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l r, f with
    | Std.DTreeMap.Internal.Impl.leaf, f => h_1 f
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r, f => h_2 size k' v' l r f) =
    h_2 size k' v' l r f