证明树排版测试

(MB (ProofTreeRender
     `(<== (cut (,Δ ,Δ^)
                ,(&⊗ $A $B)
                (,Δ^^)
                ,$C)
           (⊗R (,Δ) ,$A (,Δ^) ,$B)
           (⊗L (,Δ^^) ,$A ,$B ,$C))
     env:linear))

\frac{\frac{Δ ⊢ A Δ^{'} ⊢ B}{Δ, Δ^{'} ⊢ A \otimes B} \otimes R \frac{Δ^{″}, A, B ⊢ C}{Δ^{″}, A \otimes B ⊢ C} \otimes L}{Δ, Δ^{'}, Δ^{″} ⊢ C} {cut}_{A \otimes B}

(MB (ProofTreeRender
     `(<== (cut (,Δ^) ,$B
                (,Δ ,Δ^^) ,$C)
           (axiom
            ,(Sequent
              (list Δ^) (list $B)))
           (cut (,Δ) ,$A
                (,Δ^^ ,$B) ,$C))
     env:linear))

\frac{Δ^{'} ⊢ B \frac{Δ ⊢ A Δ^{″}, B, A ⊢ C}{Δ, Δ^{″}, B ⊢ C} {cut}_{A}}{Δ^{'}, Δ, Δ^{″} ⊢ C} {cut}_{B}