But before we move to a more expressive typed discipline, let's just have a look again at our formal system for type inference. The typing rules that we showed before for the typed l-calculus are exactly the same as the logical rules for implication in natural deduction. If you forget about the black terms here, these are just simply the rules for implication. And then you may think to these black things just as annotations for proofs in natural deduction.

---