cases f x₁ x₂ y₂ <;> dsimp <;> rw [h_ind_xs]
case a.e.e.refl
α : 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 b a_1 => f a a_1 b) x xs
ys✝ ys : KVChain r β
h_ind_ys :
  mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a b a_1 => f a a_1 b) ys (KVChain.cons x₁ x₂ xs hxs)
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 (fun a b a_1 => f a a_1 b) ys xs)
        (fun val =>
          KVChain.cons x₁ val (mergeWith (fun a b a_1 => f a a_1 b) ys xs)
            (_ : boundLeft x₁ (mergeWith (fun a b a_1 => f a a_1 b) ys xs)))
        (f x₁ x₂ y₂)).toList
no goals