apply KVChain.eq_of_toList_eq
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b₁ b₂ : β a
xs ys : KVChain r β
haxs : boundLeft a xs
hays : boundLeft a ys
⊢ mergeWith f (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays) =
    Option.casesOn (f a b₁ b₂) (mergeWith f xs ys) fun bf =>
      KVChain.cons a bf (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b₁ b₂ : β a
xs ys : KVChain r β
haxs : boundLeft a xs
hays : boundLeft a ys
⊢ (mergeWith f (KVChain.cons a b₁ xs haxs) (KVChain.cons a b₂ ys hays)).toList =
    (Option.casesOn (f a b₁ b₂) (mergeWith f xs ys) fun bf =>
        KVChain.cons a bf (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).toList