intro a₁ b₁ ys ha₁ys h_ind xs hxsys haxs
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            (insertWithAux f xs ys hxsys a b haxs).val.snd =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd)
        xs →
      (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            (insertWithAux f xs ys hxsys a b haxs).val.snd =
              (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd)
        (KVChain.cons a_1 b_1 xs haxs)
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
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.snd = (insertWithAux f KVChain.nil ys True.intro a b True.intro).val.snd
xs : KVChain (flip r) fun a => β a
hxsys : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
haxs : boundLeft a xs
⊢ (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) hxsys a b haxs).val.snd =
    (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ ys ha₁ys) True.intro a b True.intro).val.snd