Declares element: Ind → Ind → Prop to be a binary predicate symbol, with syntax x ∈ A as a shorthand for element x A. It is opaque, a primitive symbol that is characterized by axioms rather than given by a definition.