## 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.
```