根本から勘違いしている可能性があるけど、

|- _T ( x=y <-> y=x )　（ただしT はTheorem）
∵ |- _T ( x=y -> x=x -> y=y -> y=x )

この理屈が成立するには、p を T における述語として、 |- _T ( p₃xxy -> y), |- _T ( p₃yxy -> x ) となるp₃ が必要だと思うんだけど、これって自明なの？（少なくとも僕にとってはムズカシイ。）　「式中に1度しか出現しかない元を抽出できる」、さらには「式中である性質を持つ元だけを抽出できる」なんて、直感的には定理になるとは思えないんだけどねえ。