箱入り無数目の話でいえば、
選択公理を使った証明の中で
当然同値類の代表の選択関数φも決定番号ｄもでてくる

このような対象に関する言明を一切してはならない
という主張に関してはこういうしかない

定理のステートメントに現れてはならない、というのは然り
証明中に現れてはならない、というのは否

存在例化の推論規則にはっきりｃって書かれてるのがその証拠（笑）