∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : Std.DTreeMap.Internal.Impl.contains k m₂ = true),
  (m₁.union! m₂).getKey k ⋯ = m₂.getKey k mem