∀ {α : Type u} {β : α → Type v} [inst : Ord α] (sz : ℕ) (a : α) (v : β a) (l r : Std.DTreeMap.Internal.Impl α β)
  (k : α), compare k a = Ordering.lt → (k ∈ Std.DTreeMap.Internal.Impl.inner sz a v l r ↔ k ∈ l)