To define the connectives, we provide rules for using them: for example, a rule $\frac{a ; b}{c}$
matches parts of the tree that have two premises, represented by variables $a$
and $b$, and have any conclusion, represented by variable $c$.
Rules for Logical Connectives
Introduction rules say how to produce a connective. Elimination rules say how to use it.
Text in parentheses is comments. Letters are variables: stand for anything.
Try to use only the connective you define in its definition.
TODO