case cons =>
  intro a₁ b₁ xs ha₁xs _ d hdxs hda
  unfold insertWith
  dsimp [boundLeft]
  apply List.predHead_of_forAll
  rw [List.forAll_reverseAux]
  apply forAll_fst_insertWithAux
  . exact True.intro
  . apply (xs.cons a₁ b₁ ha₁xs).ascend.forAll_of_predHead
    . exact λ _ _ h₁ h₂ => trans (t:=r) h₁ h₂
    . exact hdxs
  . exact hda
α : 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)
no goals