λx: τ.e
slide
:
The subtype calculus