∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (l l_1 : Std.DTreeMap.Internal.Impl α β) (e_l : l = l_1) (h : l.Balanced),
      Std.DTreeMap.Internal.Impl.insertₘ k v l h = Std.DTreeMap.Internal.Impl.insertₘ k v_1 l_1 ⋯