conv in KVChain.cons a₁ b₁ ys ha₁ys => unfold KVChain.cons
α : 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.loop f a b xs (KVChain.cons a₁ b₁ ys ha₁ys).toList
      (_ : List.Ascending (Sigma.relOnFst r) (KVChain.cons a₁ b₁ ys ha₁ys).toList)
      (_ :
        List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
          (KVChain.cons a₁ b₁ ys ha₁ys).toList)
      haxs =
    insertWithAux.loop f a b (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys.toList
      (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
      (_ :
        List.predHead
          (fun b =>
            List.predHead (flip (fun a b => r a.fst b.fst) b) (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)).toList)
          ys.toList)
      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
hbc : r a₁ a
⊢ insertWithAux.loop f a b xs
      { toList := { fst := a₁, snd := b₁ } :: ys.toList,
          ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }.toList
      (_ :
        List.Ascending (Sigma.relOnFst r)
          { toList := { fst := a₁, snd := b₁ } :: ys.toList,
              ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }.toList)
      (_ :
        List.predHead ((fun a => boundLeft a xs) ∘ Sigma.fst)
          { toList := { fst := a₁, snd := b₁ } :: ys.toList,
              ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a₁, snd := b₁ } :: ys.toList)) }.toList)
      haxs =
    insertWithAux.loop f a b (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys.toList
      (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
      (_ :
        List.predHead
          (fun b =>
            List.predHead (flip (fun a b => r a.fst b.fst) b) (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)).toList)
          ys.toList)
      hbc