∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₁ = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) = true},
  Std.DTreeMap.Internal.Impl.Const.get (m₁.union! m₂) k h' = Std.DTreeMap.Internal.Impl.Const.get m₂ k ⋯