SetUnfold Instances for list

Hi, I have the following two instances of SetUnfoldElemOf for fmap and rev on lists that I would like to upstream to Iris, but I do not know in which file to best put them. (The proofs also use ssreflect, but I can adjust this once I know where to put the instances)

Global Instance set_unfold_rev {A} (x : A) l P: SetUnfoldElemOf x l P -> SetUnfoldElemOf x (rev l) P.
Proof.
  move => [Hr].
  constructor.
  rewrite -Hr {Hr}.
  elim: l => //= e2 l.
  set_unfold => ->.
    by naive_solver.
Qed.

Global Instance set_unfold_list_fmap {A B} (f : A -> B) (l : list A) P:
  (∀ y, SetUnfoldElemOf y l (P y)) ->
  SetUnfoldElemOf x (f <$> l) (∃ y, x = f y /\ P y).
Proof.
  move => x Hr.
  constructor.
  have {Hr} Hr: (∀ y, y ∈ l <-> (P y)) by move => y; case (Hr y).
  setoid_rewrite <-Hr => {Hr}.
  elim: l; first by set_solver.
  move => s l IH /=. set_unfold.
  rewrite IH {IH}.
  naive_solver.
Qed.