もう一つの例として、同値関係の特徴づけを与えます。
word+([ss,p],p)R … \(:\mathsf{R}\)  \(:\mathsf{T}\)  \(:\mathsf{X}\)
lower … \([\mathbin{{\sf p}}] :\mathsf{R}\) ≃ \(\forall x ( x \mathbin{{\sf p}} x )\)
lower … \([\mathbin{{\sf p}}] :\mathsf{T}\) ≃ \(\forall x , y , z ( x \mathbin{{\sf p}} y \mathbin{{\sf p}} z \Longrightarrow x \mathbin{{\sf p}} z )\)
lower … \([\mathbin{{\sf p}}] :\mathsf{X}\) ≃ \(\forall x , y ( x \mathbin{{\sf p}} y \Longrightarrow y \mathbin{{\sf p}} x )\)
word(sc,p) … \(\in\)
word(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
\([ \mathbin{\mathrm{p}} ] :\mathsf{R}\mathsf{T}\mathsf{X} \Longleftrightarrow \forall a , b \, a \mathbin{\mathrm{p}} b \Longleftrightarrow \{ x \mid x \mathbin{\mathrm{p}} a \} = \{ x \mid x \mathbin{\mathrm{p}} b \}\) \(\blacktriangleleft\) O

1 slashを使った証明

このbookでは \(\cup\) の冪等性 を目標とします。
word(ss,p) … \(\in\)
word(ss,s) … \(\cup\)
=. … \([=] \stackrel{\star\!\star}{\Leftrightarrow} [=]\)
∪. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
\(\cup\) の冪等性
\(X \cup X = X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

2 一意量化子

abbr … \(! x P\) ≈ \(\forall y , z \in \{ x \mid P \} . y = z\)
abbr … \(\exists! x P\) ≈ \(\exists x P , ! x P\)

abbr … \(! x \mathop{{\sf A}} . P\) ≈ \(! x ( x \mathop{{\sf A}} , ( P ) )\)
abbr … \(\exists! x \mathop{{\sf A}} . P\) ≈ \(\exists! x ( x \mathop{{\sf A}} , ( P ) )\)

3 word版・abbr版の比較で分かったこと

綴りについて：abbr版（構文展開だけで完結する版）は、wordG1版と同じ綴り\(!\)・\(\exists!\)を共有します。区別は使い方（構文上の位置）だけで付きます——wordG1版は \(! x ( P )\) のように直接適用し、abbr版は \(! x P\) のように大かっこで囲みます（\(\)・\(\)等、同じ綴りが複数の役割を兼ねる既存の作法と同じです）。制限付き版（\(\mathop{{\sf A}}\)で範囲を絞る形）はabbr版のみ用意されており、綴りを\(!\)・\(\exists!\)として区別します。
\(!\)（wordG1版）は、多ソート翻訳（\(\)・ \( \cdots \) ）で\(P\)が正しく展開されないバグを一度持っていました（2026-09-11に発見・修正済み）。修正前は、\(P\)を含む定義を多ソート経路で使うと「\(P\)はProver語への翻訳を持たない」という理由で拒否されていました。abbr版の\(!\)はMathel→TSL段階で展開が完結するため、そもそもこの種のバグが起きようがない設計です。
この経緯から「単ソート \( \cdots \) にも同種の欠陥が残っているのでは」という仮説を立て、 \(! x ( x = )\) という形を実際に試しました。最初は「述語が変数を参照すると証明できない」ように見えましたが、調べ直すと比較の作り方自体に誤りがありました—— \(! x ( x = \mathrm{c} )\) （通常の等号\(=\)）と \(! x ( x = w )\) （クラスの等号\(=\)）という別の述語を比較していたのです。
\(=\)は外延性を経由する定義（ \(X = Y \Longleftrightarrow ( )\) ）なので、 \(x = w\) から\(\)型の帰結を導くには外延性そのものを補助知識として使う必要があり、それを与えずに\(\)となるのは正しい挙動でした。等号を揃えて \(! x ( x = w )\) （通常の\(=\)）で試し直すと、単ソートでも正しく\(\)になり、abbr版の\(!\)と一致しました。
教訓：「動きが違う」と思ったら、まず比較している対象が本当に同じ主張かどうかを疑うこと。今回は\(=\)と\(=\)という似て非なる記号を取り違えたことが原因でした。査読が機械的に厳密である一方、人間（やAIエージェント）が書くテスト自体にも同じ厳密さが要ります。

結論として、word版\(!\)/\(\exists!\)自体に単ソートでの新しい欠陥は見つかりませんでした。ただし、実際に見つかった多ソートのバグと、バックエンドごとに展開処理を複製せずに済むabbr版の設計上の単純さ（Mathel→TSL段の構文展開1回で完結する）を踏まえ、新しくBookを書くときはabbr版（ \(! x P\) ・ \(\exists! x P\) 、制限付きなら\(!\)・\(\exists!\)）を使うことを推奨しました。現在は wordG1版\(!\)/\(\exists!\)は無く、使えるのは abbr版だけです。