Definition finds
  {A  : Set}
  (f  : A -> list A -> option A)
  (x  : A)
  (y  : A)
  (ys : list A)
: Prop :=
  f x ys = Some y <-> In y ys.
