∀ {α : Type u} {β : α → Type v} {motive : (a : Std.DTreeMap.Internal.Impl α β) → a.Balanced → Prop}
  {a : Std.DTreeMap.Internal.Impl α β} (t : a.Balanced),
  motive Std.DTreeMap.Internal.Impl.leaf ⋯ →
    (∀ {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (a : l.Balanced) (a_1 : r.Balanced)
        (a_2 : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size) (a_3 : sz = l.size + 1 + r.size),
        motive l a → motive r a_1 → motive (Std.DTreeMap.Internal.Impl.inner sz k v l r) ⋯) →
      motive a t