用于书写形式化中数理逻辑证明题
样例：
#proof(
$q->r$, [p], // premise 的缩写形式 [p]
[+], 5, // 建立一个持续 5 行的 assuption
$p->q$, [a], // assumption 的缩写形式 [a]
[+], 3, // 建立一个持续 3 行的 assuption
$p$, [a],
$q$, [$-> e$ 2,3],
$r$, [$-> e$ 1,4],
$p->r$, [$-> i$ 3-5],
$(p->q)->(p->r)$, [$-> i$ 2-6],
)
#proof(
$exists x(S->Q(x))$, [p],
[+], 5,
$S$, [a],
[+], 3,
$x_0$, [x], // 建立一个任意变量 x_0，该变量的声明将和下一行一起显示
$S->Q(x_0)$, [a],
$Q(x_0)$, [$-> e$ 3,2],
$exists x Q(x)$, [$exists x space i$ 4],
$exists x Q(x)$, [$exists x space e$ 1,3-5],
$S->exists x Q(x)$, [$-> i$ 2,6]
)
基础用法：
#proof($公式1$, [规则1], $公式2$, [规则2], $公式3$, [规则3], ...)
规则简写：
[p] = premise
[a] = assumption
[x] = new variable
其他简写：
[+] = new block
定义一个 assumption 块（作用域）：
#proof(
...
[+], 作用域大小,
$作用域中的公式1$, [作用域中的规则1],
...
)
定义一个变量，并令该变量的声明和公式 n 处于同一行：
#proof(
...
$变量名$, [x],
$公式n$, [规则n],
...
)
定义一个变量，该变量的声明位于单独一行：
#proof(
...
$变量名$, [x],
$$, [],
...
)
Warning: 不支持换页排版，请自行换页