我要问一个很蠢的问题：
|- P <-> Q
该怎么拆解？
发现它并不存在于 sequent calculus 的规则内
难道说我只能把它转成
|- (P->Q) Λ (Q->P) 来做吗？
（而且这样还不能写这是哪一条规则！只能说by definition <-> is xxxxx）

就根据定义啊，把 P<->Q 定义成底下的形式没问题。证明也是会 by theorem 来引用，不可能每次都从头推到尾

谢谢 第一次写这种证明，所以有点战战兢兢XD