∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ (k : α) (f : Option β → Option β),
          (Std.DTreeMap.Raw.Const.alter t₁ k f).Equiv (Std.DTreeMap.Raw.Const.alter t₂ k f)