. rw [cons_mergeWith_cons_rel hx₁y₁]
  rw [cons_mergeWith_cons_rel hx₁y₁]
  dsimp
  rw [h_ind_xs]
case a.t
α : 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✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith g xs x
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 g (KVChain.cons x₁ x₂ xs hxs) ys
hx₁y₁ : r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList

case a.e
α : 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✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith g xs x
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 g (KVChain.cons x₁ x₂ xs hxs) ys
hx₁y₁ : ¬r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList
case a.e
α : 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✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith g xs x
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 g (KVChain.cons x₁ x₂ xs hxs) ys
hx₁y₁ : ¬r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList