Let Binding
Backlinks
Cut Rule
Bidirectional Type Theory