Theorem intersectionPairsIn : forall (A : Set) (ea eb : list A) efa efb f,
  (forall x y ys, finds f x y ys) ->
    In (efa, efb) (intersectionPairs f ea eb) ->
      In efa ea /\ In efb eb.
Proof.
  (* Proof omitted for brevity; see Intersection.v for proofs. *)
Qed.
