rw [insertWith_nil]
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a✝¹ : α
b : β a✝¹
a : α
a✝ : boundLeft a KVChain.nil
hab : r a a✝¹
⊢ boundLeft a (insertWith f KVChain.nil a✝¹ b)
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a✝¹ : α
b : β a✝¹
a : α
a✝ : boundLeft a KVChain.nil
hab : r a a✝¹
⊢ boundLeft a
    { toList := [{ fst := a✝¹, snd := b }],
      ascend := (_ : List.Ascending (Sigma.relOnFst r) [{ fst := a✝¹, snd := b }]) }