rw [nil_mergeWith, nil_mergeWith]
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ f g : (a : α) → β a → β a → Option (β a)
hfg : ∀ (a : α) (b₁ b₂ : β a), f a b₁ b₂ = g a b₁ b₂
xs ys x✝ : KVChain r β
⊢ mergeWith f KVChain.nil x✝ = mergeWith g KVChain.nil x✝
no goals