∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp]
  {mergeFn : (a : α) → β a → β a → β a} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.WF → (Std.DTreeMap.Raw.mergeWith mergeFn t₁ t₂).WF