∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DTreeMap.Raw.Const.get? (m₁ ∪ m₂) k = Std.DTreeMap.Raw.Const.get? m₂ k