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

case cons
α : 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_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun xs => ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)) xs →
      (fun xs => ∀ (d : α), boundLeft d xs → r d a → boundLeft d (insertWith f xs a b)) (KVChain.cons a_1 b_1 xs haxs)