dsimp
case a.e.t
α : 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 β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ (KVChain.cons y₁ y₂ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys)
        (_ : boundLeft y₁ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys))).toList =
    (KVChain.cons y₁ y₂ (mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs))
        (_ : boundLeft y₁ (mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)))).toList
case a.e.t
α : 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 β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ { fst := y₁, snd := y₂ } :: (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys).toList =
    { fst := y₁, snd := y₂ } :: (mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)).toList