revert xs
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
ys : KVChain r β
hxsys : hingeable xs ys
a : α
b : β a
haxs : boundLeft a xs
⊢ (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
    (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
⊢ ∀ {xs : KVChain (flip r) β} {hxsys : hingeable xs ys} {haxs : boundLeft a xs},
    (insertWithAux f xs ys hxsys a b haxs).val.fst.toList =
      (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.fst.toList ++ xs.toList