∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ (f : (a : α) → β a → Bool), (Std.DTreeMap.Raw.filter f t₁).Equiv (Std.DTreeMap.Raw.filter f t₂)