apply ys.recOnList (motive:=λ ys => ∀ xs haxs hays, mergeWith f (xs.cons a b haxs) ys = (mergeWith f xs ys).cons a b (boundLeft_mergeWith a haxs hays))
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
ys : KVChain r β
⊢ ∀ {xs : KVChain r β} {haxs : boundLeft a xs} (hays : boundLeft a ys),
    mergeWith f (KVChain.cons a b xs haxs) ys =
      KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
ys : KVChain r β
⊢ ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a KVChain.nil),
    mergeWith f (KVChain.cons a b xs haxs) KVChain.nil =
      KVChain.cons a b (mergeWith f xs KVChain.nil) (_ : boundLeft a (mergeWith f xs KVChain.nil))

case cons
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a : α
b : β a
ys : KVChain r β
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a ys),
            mergeWith f (KVChain.cons a b xs haxs) ys =
              KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys)))
        xs →
      (fun ys =>
          ∀ (xs : KVChain r fun a => β a) (haxs : boundLeft a xs) (hays : boundLeft a ys),
            mergeWith f (KVChain.cons a b xs haxs) ys =
              KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys)))
        (KVChain.cons a_1 b_1 xs haxs)