\lambda x.x y ((\lambda x.x) y) lambda > apply
S x = y (= (S x) y) apply > infix operators
\forall x.x=x (\forall x.(= x x)) infix operators > binders
+\lambda x.x \to x \lambda. (x \to x) \to > \lambda
--------------------------------------------------------------------------------
Precedence total order:
- lambda > apply > infix operators > binders
+ \to > lambda > apply > infix operators > binders
where binders are all binders except lambda (i.e. \forall, \pi, \exists)