$`\lambda`$ や $`\forall`$ は省略されることが多い。$`\forall`$ に関しては次の2つのケースがある。
- モノグサ： 書くのがめんどくさいから省略。
- 推論規則： 全称限量子 $`\forall`$ の消去〈elimination〉規則を適用した。
証明の途中で全称限量子は正式な手順として消去して〈取り去って〉よいが、このときもモノグサ行為が行われる。ありとあらゆる所でモノグサ行為は行われている。緊張感と注意力を高めた状態でないと、モノグサ行為の背後の事実を読み取れない。$`\newcommand{\Then}{\downdownarrows}
\newcommand{\Imp}{\Rightarrow}
%`$
証明図（が書けない）
論理の証明図は横棒で書くが、MathJaxではうまく横棒が書けないので、代わりに $`{\Then}`$ を使う。例えば：
$`\vdash P\quad \vdash Q\\
\Then\\
\vdash (P \land Q)
`$
ここで、$`\vdash`$ は「公理か、または既に証明済みである。」という意味。日本語混じりで書くなら：
$`P`$ は公理か、または既に証明済みである。$`Q`$ は公理か、または既に証明済みである。
よって、
$`(P \land Q)`$ は証明済みとなる。
$`\vdash`$ もモノグサで省略されるから、
$`P\quad Q\\
\Then\\
P \land Q
`$
全称限量子の消去
次は正式に許される。
$`\forall x\in X.P(x)\\
\Then\\
P(x)
`$
が、これはモノグサされていて、実際には暗黙の文脈〈コンテキスト〉がある。コンテキストを大きなブラケットで書くと：
$`\big[\cdots\big]\; \forall x\in X.P(x)\\
\Then\\
\big[\cdots,\; x\in X\big]\; P(x)
`$
束縛変数 $`x`$ を自由変数にしてよいが、自由変数の型〈プロファイル | 所在〉の情報は必ず暗黙のコンテキストに入れる。暗黙のコンテキストは、書かれてなくても心のなかで追跡し続ける（名前追跡）。
リネームと名前のバッティング
束縛変数はリネームしてよい。
$`\forall y, y'\in Y.( y\le x' \Imp g(y)\le g(y') )\\
\Then\\
\forall x, x'\in Y.( x\le x'\Imp g(x)\le g(x') )
`$
リネーム後に全称限量子を消去すると：
$`\forall y, y'\in Y.( y\le x' \Imp g(y)\le g(y') )\\
\Then\\
\forall x, x'\in Y.( x\le x'\Imp g(x)\le g(x') )\\
\Then\\
x\le x'\Imp g(x)\le g(x')
`$
これだけだと何も問題ないが、暗黙のコンテキスト内に $`x, x'`$ が既に入っているならダメ。
$`\big[\cdots,\; x, x'\in X \big]\; \forall y, y'\in Y.( y\le x' \Imp g(y)\le g(y') )\\
\Then\\
\big[\cdots,\; x, x'\in X \big]\; \forall x, x'\in Y.( x\le x'\Imp g(x)\le g(x') )\\
\Then\\
\big[\cdots,\; x, x'\in X,\; x, x'\in Y \big]\; x\le x'\Imp g(x)\le g(x')
`$
暗黙のコンテキスト（大きなブラケット）内で、名前と型がワヤクチャになっている。暗黙のコンテキストも含めて名前管理をしなくてはいけない。
名前の追跡・分析・管理は、最も重要な作業なのだが、無頓着な人がいる。名前に対する緊張感と注意力が低すぎる。それじゃダメだ。
自由変数には代入してよい
暗黙のコンテキストも含めて、名前と型が整合的なら、自由変数には代入をしてよい。
$`\big[\cdots,\; x, x'\in X \big]\; \forall y, y'\in Y.( y\le x' \Imp g(y)\le g(y') )\\
\Then\\
\big[\cdots,\; x, x'\in X,\; y, y'\in Y \big]\; y\le y'\Imp g(y)\le g(y') \\
\Then y := f(x), y' := f(x') \: \text{ 代入}\\
\big[\cdots,\; x, x'\in X \big]\; f(x)\le f(x')\Imp g( f(x) )\le g( f(x') )
`$
このとき、暗黙のコンテキストの $`\cdots`$ のなかに、$`f(x), f(x')\in Y`$ が入ってないといけない。また、名前〈変数名〉$`y, y'`$ は代入で消えているので、暗黙のコンテキスト内からも $`y, y'`$ の情報は消す。
証明を遂行する際には、暗黙のコンテキストを意識しながら、暗黙のコンテキストに対してかなり複雑な操作をしている。間違いなくやるためには、モノグサしないで暗黙のコンテキストも明示的に書き出すのが良い方法である。書き出す量が増えるが、どのくらい増えるかを経験しておくべき。
慣れてる人／頭の良い人は書き出さないで（いわば暗算で）処理できるが、慣れてない人間がイキナリ暗算は無理。無理なことを闇雲にやろうとするから結局は間違う／出来ない。慣れるまでは、暗黙情報を書き出そう。
