∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  (t t_1 : Std.ExtDTreeMap α β cmp), t = t_1 → ∀ (a : α) (f f_1 : β a → β a), f = f_1 → t.modify a f = t_1.modify a f_1