case cons =>
  intro a₁ b₁ xs ha₁xs _ h_ind_ys hda₁
  dsimp [boundLeft, hingeable, mergeWith, mergeWith.loop]
  rw [toList_mergeWith_loop_eq_reverseAux]
  apply dite (r a₁ a₂) <;> intro ha₁a₂
  . rw [insertWithAux_cons_rel ha₁a₂]
    rw [toList_fst_insertWithAux_eq_append]
    rw [List.reverseAux_append_left]
    dsimp [List.reverse, List.reverseAux]
    exact hda₁
  . apply dite (r a₂ a₁) <;> intro ha₂a₁
    . rw [insertWithAux_cons_flip ha₂a₁]
      dsimp [List.reverseAux]
      exact hda₂
    . have : a₂ = a₁ := Trichotomous.eq_of_incomp ⟨ha₂a₁, ha₁a₂⟩
      cases this
      rw [insertWithAux_cons_rfl]
      cases f a₂ b₁ b₂ <;> dsimp
      case none =>
        apply h_ind_ys
        . exact boundLeft_descend (λ _=> trans hda₂) ha₁xs
        . exact boundLeft_descend (λ _=> trans hda₁) ha₂ys
      case some bf =>
        dsimp [List.reverseAux, List.predHead]
        exact hda₂
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
d : α
ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r fun a => β a
ha₂ys : boundLeft a₂ ys
xs : KVChain r fun a => β a
hda₂ : boundLeft d (KVChain.cons a₂ b₂ ys ha₂ys)
⊢ ∀ (a : α) (b : β a) (xs : KVChain r fun a => β a) (haxs : boundLeft a xs),
    (fun xs =>
          (∀ (xs₁ : KVChain r fun a => β a), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)) →
            boundLeft d xs → boundLeft d (mergeWith f xs (KVChain.cons a₂ b₂ ys ha₂ys)))
        xs →
      (fun xs =>
          (∀ (xs₁ : KVChain r fun a => β a), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)) →
            boundLeft d xs → boundLeft d (mergeWith f xs (KVChain.cons a₂ b₂ ys ha₂ys)))
        (KVChain.cons a b xs haxs)
no goals