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✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ mergeWith f (KVChain.cons a b✝ x hax) (KVChain.cons b y hby hpb) =
    KVChain.cons a b✝ (mergeWith f x (KVChain.cons b y hby hpb))
      (_ : boundLeft a (mergeWith f x (KVChain.cons b y hby hpb)))
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b✝ : β a
ys : KVChain r β
b : α
y : β b
hby : KVChain r fun a => β a
hpb : boundLeft b hby
a✝ :
  ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a hby),
    mergeWith f (KVChain.cons a b✝ xs haxs) hby =
      KVChain.cons a b✝ (mergeWith f xs hby) (_ : boundLeft a (mergeWith f xs hby))
x : KVChain r fun a => β a
hax : boundLeft a x
hab : boundLeft a (KVChain.cons b y hby hpb)
⊢ (mergeWith f (KVChain.cons a b✝ x hax) (KVChain.cons b y hby hpb)).toList =
    (KVChain.cons a b✝ (mergeWith f x (KVChain.cons b y hby hpb))
        (_ : boundLeft a (mergeWith f x (KVChain.cons b y hby hpb)))).toList