intro hbc
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
⊢ ∀ (ha₁a : r a₁ a),
    insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs =
      insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
        (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b ha₁a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a₁ : α
b₁ : β a₁
ys : KVChain r β
ha₁ys : boundLeft a₁ ys
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
a : α
b : β a
haxs : boundLeft a xs
hbc : r a₁ a
⊢ insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b haxs =
    insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
      (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b hbc