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