Li-Fan Chen says to YSITD
sequent calculus 跟 natural deduction 的差別是什麼