opaque コマンドの説明を見直して読みやすくする

Examples/Command/Declarative/Opaque.lean

@@ -1,7 +1,9 @@
 /- # opaque
-`opaque` は、定義に展開できない名前を宣言するコマンドです。
+`opaque` は、定義に展開できない名前を宣言するコマンドです。具体的な実装を与えずに特定の型を持つ項が「とりあえず何かある」という表現ができます。
 
-`opaque` コマンドを使用して宣言した名前は、`#reduce` コマンドで簡約できません。
+## def との違い
+
+[`def`](./Def.md) と異なり `opaque` コマンドを使用して宣言した名前は、`#reduce` コマンドで簡約できません。
 -/
 
 -- def を使って定義
@@ -74,8 +76,8 @@ Additional diagnostic information may be available using the `set_option diagnos
 -/
 #guard_msgs in opaque something : Something
 
-/- ## 使用例
-具体的に値を与えずに型だけを指定することができるため、「...という要件を満たす何かが、とにかく存在すると仮定する」という表現ができます。
+/- ## variable との違い
+`opaque` と同じく [`variable`](./Variable.md) コマンドも「特定の型を持つ項がとりあえず何かある」という表現をするために使用されることがありますが、両者には重要な違いがあります。
 
 たとえば、Lean の型システムにおいて「自分自身に適用することができる関数 `f : (A → B) → C` は存在しない」ということをコードで確かめたかったとします。このとき「何でもいいので」型 `A, B, C` と関数 `f` が存在すると仮定を置きたくなります。