I hope there is some agreed notation for this. The idea is very similar to DOM (or CSS) selectors, but on mathematical (or logical) formulas. I'll explain this with an example.
Imagine I have some structure, for example a sequence $S$ composed of resolution steps, each one containing input sentences and resolvents (usually one resolvent). These sentences are implications (with a head and a body). Head and body have several atoms (normally only one in the head), which have several terms, which may be constants, variables or functions applied to terms.
I want to speak about those constants in $S$ (in fact in fragments of it, $\{S_{\alpha_1}^{\omega_1}, \ldots, S_{\alpha_n}^{\omega_n}\}$, I hope that doesn't make a difference). Certainly $c:constant \in S$ is not an option, since $S$ "contains" no constants (technically $S$ is a sequence of resolution steps).
I was considering to use something like $c:constant\ of\ S$. Other options are: $c \in constants(S)$ or something fancy like $c:constant \bar{\in} S$. I guess I have to specify the type of $c$ to say what am I talking about (I hope I'm doing that right).
There is no notation for this kind of thing in my area, AFAIK, and I'm not aware of anything similar in any other area, except DOM and CSS selectors (maybe lenses for functional programming).
How should I represent that? (Or should I avoid this kind of notation?)
If you want to be precise, a good way would be to define a mapping:
$$\operatorname{const}: {\sf Sequences} \to \mathcal P({\sf Constants})$$
assigning to a sequence $S$ the set of constants occurring in $S$ (which you can determine recursively). Then you can write $c \in \operatorname{const}(S)$ as in one of your suggestions.
The other options are a bit awkward from a mathematical point of view. They are reminiscent of type theory, but even in that context it is a bit odd, since the "type" of $c$ is more naturally "constant" than "constant of $S$".