∀ {α : Type u} {β : α → Type v} (k : α) (v : β k)
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf
      (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf) →
    (∀ (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')
          (Std.DTreeMap.Internal.Impl.balanceR! k' v' l' (Std.DTreeMap.Internal.Impl.insertMax! k v r'))) →
      ∀ (t : Std.DTreeMap.Internal.Impl α β), motive t (Std.DTreeMap.Internal.Impl.insertMax! k v t)