dsimp [insertWithAux, insertWithAux.loop]
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
xs : KVChain (flip r) fun a => β a
hxsys : hingeable xs KVChain.nil
haxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
a✝ : List.forAll (p ∘ Sigma.fst) KVChain.nil.toList
hpa : p a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.snd.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
p : α → Prop
xs : KVChain (flip r) fun a => β a
hxsys : hingeable xs KVChain.nil
haxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
a✝ : List.forAll (p ∘ Sigma.fst) KVChain.nil.toList
hpa : p a
⊢ List.forAll (p ∘ Sigma.fst) ({ fst := a, snd := b } :: xs.toList) ∧ List.forAll (p ∘ Sigma.fst) []