suffices (insertWithAux f KVChain.nil xs True.intro a b True.intro).val = (⟨[⟨a,b⟩],List.Ascending.singleton _⟩,xs) by
  rw [this]; rfl
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : boundLeft a xs
⊢ List.reverseAux (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil xs True.intro a b True.intro).val.snd ys).toList =
    (KVChain.cons a b (mergeWith f xs ys) (_ : boundLeft a (mergeWith f xs ys))).toList
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain r β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : boundLeft a xs
⊢ (insertWithAux f KVChain.nil xs True.intro a b True.intro).val =
    ({ toList := [{ fst := a, snd := b }],
        ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) [{ fst := a, snd := b }]) },
      xs)