∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α]
  [inst_3 : (k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)] (t₁ t₂ : Std.DTreeMap.Internal.Impl α β),
  t₁.WF → t₂.WF → (t₁.beq t₂ = true ↔ t₁.Equiv t₂)