apply ys.recOnList (motive:=λ ys=> ∀ xs, xs.boundLeft d → ys.boundLeft d → (mergeWith f xs ys).boundLeft d)
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
d : α
ys : KVChain r β
⊢ ∀ {xs : KVChain r β}, boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys)
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
d : α
ys : KVChain r β
⊢ ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d KVChain.nil → boundLeft d (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)
d : α
ys : KVChain r β
⊢ ∀ (a : α) (b : β a) (xs : KVChain r fun a => β a) (haxs : boundLeft a xs),
    (fun ys => ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys)) xs →
      (fun ys => ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys))
        (KVChain.cons a b xs haxs)