>>318
普通のんでいいです。
∀　導入規則で検索したらこんなのがあったので、これでいいです。
∀-導入
Aa
-------(∀-導入)
∀x　A
aは結論には現れない自由変数

ふと思ったのですが、
a+0=a、b+0=b、・・・（a、b、・・は定項）が証明可能であるとき、
x+0=x（xは自由変項）が証明可能、（便宜的にそう書き表してよい、とかいうのではなしに、論理式として証明可能）
というようなこと、形式的体系の（自明な？）規則としてあります？