{α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive : (t : Std.DTreeMap.Internal.Impl α β) → Std.DTreeMap.Internal.Impl.contains k t = true → Sort u_3) →
          (t : Std.DTreeMap.Internal.Impl α β) →
            (hlk : Std.DTreeMap.Internal.Impl.contains k t = true) →
              ((size : ℕ) →
                  (k' : α) →
                    (v : β k') →
                      (l r : Std.DTreeMap.Internal.Impl α β) →
                        (hlk :
                            Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
                              true) →
                          motive (Std.DTreeMap.Internal.Impl.inner size k' v l r) hlk) →
                motive t hlk