case cons =>
  intro a₂ b₂ ys ha₂ys h_ind_ys xs hdxs hda₂
  revert h_ind_ys hdxs
  apply xs.recOnList (motive:=λ xs=> (∀ xs₁, xs₁.boundLeft d → ys.boundLeft d → (mergeWith f xs₁ ys).boundLeft d) → xs.boundLeft d → (mergeWith f xs (ys.cons a₂ b₂ ha₂ys)).boundLeft d)
  case nil => rw [nil_mergeWith]; exact λ _ _=> hda₂
  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) (xs : KVChain r fun a => β a) (haxs : boundLeft a xs),
    (fun ys => ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys)) xs →
      (fun ys => ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys))
        (KVChain.cons a b xs haxs)
no goals