# Difference between revisions of "Generic Instantiation"

Currently, the proposal mentions that the carrier sets can be instantiated to any set expressions (which contains existing carrier sets and constants). Beside the declared axioms in the development to be extended there are two hidden axioms about a carrier set S<code> 
$  S \neq \emptyset$ $\forall x \qdot x \in S$ Both these axioms can be generated as theorems in the instantiating context which need to be proved. 
However, the second theorem can be proved if <code>S is instantiated to another carrier set in the instantiating context.