simp
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs ys x✝ : KVChain r β
⊢ mergeWith f KVChain.nil x✝ = mergeWith (fun a => flip (f a)) x✝ KVChain.nil
no goals