∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} [inst : Std.TransCmp cmp]
  (t : Std.ExtDTreeMap α (fun x => β) cmp) (a : α) (h : a ∈ t) (x x_1 : Std.DTreeMap α (fun x => β) cmp)
  (x_2 : t = Std.ExtDTreeMap.mk x),
  t = Std.ExtDTreeMap.mk x_1 → ∀ (h_1 : x.Equiv x_1), Std.DTreeMap.Const.get x a ⋯ = Std.DTreeMap.Const.get x_1 a ⋯