Disclaimer: I know close to nothing about formal type theory, but I program intensively so prefer to think in terms of types.
In typical math you write $a \in A$ to speak of the nature of your objects or elements. However, I prefer to think instead of types and list, which is more common in computer science.
I would like to write something like
$$a : A $$ $$l : List \hspace{1 mm}A$$ $$a \in l$$
While I would be able to understand myself, I want to make sure other also understand me, what notation can I use?