rw [insertWithAux_cons_rfl]
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (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
xs : KVChain (flip r) fun a => β a
haxs : boundLeft a xs
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
ha₁a haa₁ : ¬r a a
⊢ (Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
            { val := (KVChain.cons a bf xs haxs, ys),
              property :=
                (_ : hingeable (KVChain.cons a bf xs haxs) (KVChain.cons a bf xs haxs, ys).snd) }).val.fst.toList =
    (insertWithAux f KVChain.nil (KVChain.cons a b₁ ys ha₁ys) True.intro a b True.intro).val.fst.toList ++ xs.toList
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (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
xs : KVChain (flip r) fun a => β a
haxs : boundLeft a xs
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
ha₁a haa₁ : ¬r a a
⊢ (Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
            { val := (KVChain.cons a bf xs haxs, ys),
              property :=
                (_ : hingeable (KVChain.cons a bf xs haxs) (KVChain.cons a bf xs haxs, ys).snd) }).val.fst.toList =
    (Option.casesOn (f a b₁ b)
              { val := (KVChain.nil, ys), property := (_ : hingeable (KVChain.nil, ys).fst (KVChain.nil, ys).snd) }
              fun bf =>
              { val := (KVChain.cons a bf KVChain.nil True.intro, ys),
                property :=
                  (_ :
                    hingeable (KVChain.cons a bf KVChain.nil True.intro)
                      (KVChain.cons a bf KVChain.nil True.intro, ys).snd) }).val.fst.toList ++
      xs.toList