∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {k : α},
  t.WF → ((∀ (k' : α), t.minKey? = some k' → (compare k k').isLE = true) ↔ ∀ k' ∈ t, (compare k k').isLE = true)