rw [nil_mergeWith]
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
⊢ { fst := a, snd := b } :: ys.toList = { fst := a, snd := b } :: (mergeWith f KVChain.nil ys).toList
no goals