＞述語P(x)を「xはしっぽ同値類の代表選択関数」と定義。
＞選択公理から ∃xP(x) を推論でき、
＞これと存在例化推論規則から P(c) を推論できる。
＞名前cは証明内で自由に使ってよい。

そこが問題になってるわけではないと思うが