Input Should be parsed as Derived constraint
on precedence
--------------------------------------------------------------------------------
-\lambda x.x y ((\lambda x.x) y) binder > apply
+\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:
- binder > apply > infix operators
+ \to > lambda > apply > infix operators > binders
+
+where binders are all binders except lambda (i.e. \forall, \pi, \exists)