∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] (k : α)
  (f f_1 : Option (β k) → Option (β k)),
  f = f_1 →
    ∀ (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (h : t.Balanced),
      Std.DTreeMap.Internal.Impl.alterₘ k f t h = Std.DTreeMap.Internal.Impl.alterₘ k f_1 t_1 ⋯