Currying

For notational convenience with curried functions, we allow

xy.E

as an abbreviation for

x.y.E

Example:

(xy.(x (x y)) P Q)

(y.(P (P y)) Q)

(P (P Q))