∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} (hk : k ∈ t₁),
  Std.DTreeMap.Internal.Impl.Const.get t₁ k hk = Std.DTreeMap.Internal.Impl.Const.get t₂ k ⋯