intro ha₁a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
⊢ ∀ (ha₁a : r a₁ a),
    insertWith f (KVChain.cons a₁ b₁ xs ha₁xs) a b =
      KVChain.cons a₁ b₁ (insertWith f xs a b) (_ : boundLeft a₁ (insertWith f xs a b))
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
a₁ : α
b₁ : β a₁
xs : KVChain r β
ha₁xs : boundLeft a₁ xs
a : α
b : β a
ha₁a : r a₁ a
⊢ insertWith f (KVChain.cons a₁ b₁ xs ha₁xs) a b =
    KVChain.cons a₁ b₁ (insertWith f xs a b) (_ : boundLeft a₁ (insertWith f xs a b))