rw [hfg]
case a.e.e.refl
α : 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✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
y₂ : β x₁
hys : boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬r x₁ x₁
⊢ (Option.rec (mergeWith f xs ys)
        (fun val => KVChain.cons x₁ val (mergeWith f xs ys) (_ : boundLeft x₁ (mergeWith f xs ys)))
        (f x₁ x₂ y₂)).toList =
    (Option.rec (mergeWith g xs ys)
        (fun val => KVChain.cons x₁ val (mergeWith g xs ys) (_ : boundLeft x₁ (mergeWith g xs ys))) (g x₁ x₂ y₂)).toList
case a.e.e.refl
α : 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✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
y₂ : β x₁
hys : boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬r x₁ x₁
⊢ (Option.rec (mergeWith f xs ys)
        (fun val => KVChain.cons x₁ val (mergeWith f xs ys) (_ : boundLeft x₁ (mergeWith f xs ys)))
        (g x₁ x₂ y₂)).toList =
    (Option.rec (mergeWith g xs ys)
        (fun val => KVChain.cons x₁ val (mergeWith g xs ys) (_ : boundLeft x₁ (mergeWith g xs ys))) (g x₁ x₂ y₂)).toList