intros
α : 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)
α : 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
a✝¹ : boundLeft d xs✝
a✝ : boundLeft d KVChain.nil
⊢ boundLeft d (mergeWith f xs✝ KVChain.nil)