 As discussed in section 1, the step from classical ZF to its intuitionistic variants requires us to choose a suitable formulation for each set-theoretic axiom: one classical  axiom may have a number of intuitionistic variants which turn out to be  non-equivalent to each other. This is sometimes reflected by the proof-theoretic strength of the resulting theories, which may vary depending on which principles we choose.  For example, we already noted that  in CZF we do not have full separation and power set, which are  replaced by the predicatively acceptable principles of bounded separation and  subset collection, respectively. However, if we add to CZF either of these principles, we obtain impredicative theories. The impredicativity of the resulting theories is witnessed  by the fact that their proof-theoretic strenght far exceeds that of CZF.