Definition map_sum {A B B' : Type} (f : B -> B') (x : A + B) : A + B' :=
  match x with
  | inl a => inl a
  | inr b => inr (f b)
  end.

Fixpoint _find_or {A B C} (eqb : A -> A -> bool) (a : A) (xs : list (A * B)) (f : B -> C) (b : C) : C :=
  match xs with
  | nil => b
  | (x, y) :: xs => if eqb a x then f y else _find_or eqb a xs f b
  end.

Definition _bind_sum {A B C} (x : A + B) (f : B -> A + C) : A + C :=
  match x with
  | inl a => inl a
  | inr b => f b
  end.

Lemma app_cons_assoc {A} (xs : list A) (x : A) (ys : list A)
  : xs ++ x :: ys = (xs ++ [x]) ++ ys.
Proof.
  rewrite <- app_assoc; reflexivity.
Qed.