∀ {α : Type u} {β : Type v} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β) → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf none →
    (∀ (size : ℕ) (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) (some (k, v))) →
      (∀ (size : ℕ) (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
          (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
              (Std.DTreeMap.Internal.Impl.Const.minEntry? (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
              (Std.DTreeMap.Internal.Impl.Const.minEntry? (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r))) →
        ∀ (a : Std.DTreeMap.Internal.Impl α fun x => β), motive a (Std.DTreeMap.Internal.Impl.Const.minEntry? a)