{α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.lt) → Sort u_3) →
          (x : Std.DTreeMap.Internal.Impl α β) →
            (x_1 : x.Ordered) →
              (x_2 : ∃ a ∈ x, compare a k = Ordering.lt) →
                ((x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
                    (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.lt) →
                      motive Std.DTreeMap.Internal.Impl.leaf x he) →
                  ((size : ℕ) →
                      (ky : α) →
                        (y : β ky) →
                          (l r : Std.DTreeMap.Internal.Impl α β) →
                            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
                              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.lt) →
                                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he) →
                    motive x x_1 x_2