proposition: Lemma elem_of_list_fmap_2 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
proof: Proof. induction l as [|y l IH]; simpl; inv 1. - exists y. split; [done | by left]. - destruct IH as [z [??]]; [done|]. exists z. split; [done | by right]. Qed.
imports: stdpp(options)