Notation:
We use the following abbreviation: (let x = e1 in e2) for (?x.e2)e1
Call this a let expression. It makes strict applications more readable because its “argument first” appearance matches the argument first simplification strategy that must be used.