case cons =>
  intro a₁ b₁ ys ha₁ys h_ind xs ha₁xs haxs
  apply dite (r a₁ a) <;> intro ha₁a
  . rw [insertWithAux_cons_rel ha₁a]
    exact h_ind _ (cons_hingeable.symm ▸ ha₁ys) (by exact ha₁a)
  . apply dite (r a a₁) <;> intro haa₁
    . rw [insertWithAux_cons_flip haa₁]
      exact hac
    . have : a = a₁ := Trichotomous.eq_of_incomp ⟨haa₁, ha₁a⟩
      cases this
      rw [insertWithAux_cons_rfl]
      cases f a b₁ b
      case none =>
        apply boundLeft_descend _ haxs
        exact λ _ => flip (trans (r:=r) (s:=r) (t:=r)) hac
      case some bf => exact hac
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
c : α
hac : r a c
⊢ ∀ (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),
            boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst)
        xs →
      (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            boundLeft c (insertWithAux f xs ys hxsys a b haxs).val.fst)
        (KVChain.cons a_1 b_1 xs haxs)
no goals