我要問一個很蠢的問題：
|- P <-> Q
該怎麼拆解？
發現它並不存在於 sequent calculus 的規則內
難道說我只能把它轉成
|- (P->Q) Λ (Q->P) 來做嗎？
（而且這樣還不能寫這是哪一條規則！只能說by definition <-> is xxxxx）

就根據定義啊，把 P<->Q 定義成底下的形式沒問題。證明也是會 by theorem 來引用，不可能每次都從頭推到尾

謝謝 第一次寫這種證明，所以有點戰戰兢兢XD