Elimination Rule
Backlinks
Sequent Calculus
Left Rule
Negative Connective
Bidirectional Type Theory