case nil =>
  intro a _ hab
  rw [insertWith_nil]
  exact hab
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
⊢ ∀ (d : α), boundLeft d KVChain.nil → r d a → boundLeft d (insertWith f KVChain.nil a b)
no goals